Zobrazeno 1 - 10
of 232
pro vyhledávání: '"Logical Frameworks"'
Autor:
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto
Publikováno v:
Journal of Formalized Reasoning, Vol 12, Iss 1, Pp 11-51 (2019)
We develop the metatheory and the implementation of LF+, and discuss several applications. LF+ capitalizes on research work, carried out by the authors over more than a decade, on Logical Frameworks. It builds on various conservative extensions of LF
Externí odkaz:
https://doaj.org/article/bf5a22847c914ec6bcdc44be3cd63e39
Publikováno v:
Journal of Formalized Reasoning, Vol 8, Iss 1, Pp 49-91 (2015)
When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effo
Externí odkaz:
https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71
Autor:
Felicissimo, Thiago
Publikováno v:
FSCD 2022-7th International Conference on Formal Structures for Computation and Deduction
FSCD 2022-7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.25⟩
FSCD 2022-7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.25⟩
Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed unti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0cb45f28a349a130ef7f66443b96e721
Publikováno v:
Studia Logica: An International Journal for Symbolic Logic, 1998 Jan 01. 60(1), 161-208.
Externí odkaz:
https://www.jstor.org/stable/20015959
Autor:
Matteo Cristani, Claudio Tomazzoli
Publikováno v:
Current Trends in Web Engineering ISBN: 9783030512521
ICWE Workshops
ICWE Workshops
Data anonymization is the process of making information contained in a group of data such that it is not possible to identify unique references to single elements in the group after the process. This action, when conducted onto datasets used to make
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b3ee43ddcbecbed69ef35436825e7afe
https://doi.org/10.1007/978-3-030-51253-8_9
https://doi.org/10.1007/978-3-030-51253-8_9
Autor:
Genestier, Guillaume
Publikováno v:
FSCD-5th International Conference on Formal Structures for Computation and Deduction
FSCD-5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.31⟩
FSCD-5th International Conference on Formal Structures for Computation and Deduction, Jun 2020, Paris, France. ⟨10.4230/LIPIcs.FSCD.2020.31⟩
International audience; We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the ro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::41380c482e1b78df3a5e3b791094f4f3
https://inria.hal.science/hal-03838613/document
https://inria.hal.science/hal-03838613/document
Autor:
Chen, Joshua
Publikováno v:
12th International Conference on Interactive Theorem Proving
This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle's existing logical framework infrastructure to implement essential automation, suc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::42f2279a1dc7a63505712516e36c55ce
http://arxiv.org/abs/2002.09282
http://arxiv.org/abs/2002.09282
Publikováno v:
LSFA
Repositório Institucional da UFRN
Universidade Federal do Rio Grande do Norte (UFRN)
instacron:UFRN
Repositório Institucional da UFRN
Universidade Federal do Rio Grande do Norte (UFRN)
instacron:UFRN
HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a comm
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::226afe9b803f9776d2c7cb6c25cfdc92
https://doi.org/10.1016/j.entcs.2017.04.007
https://doi.org/10.1016/j.entcs.2017.04.007