The ∆-framework
| Autor: | Honsell, F., Liquori, L., Stolze, C., Scagnetto, I. |
|---|---|
| Přispěvatelé: | Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), European Project: COST Action CA15123 ,COST - European Cooperation in Science and Technology,EUTYPES(2016) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Logic of programs
Type theory λ-calculus TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] |
| Zdroj: | 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS) 2018 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS) 2018, Dec 2018, Ahmedabad, India. pp.37:1--37:21, ⟨10.4230/LIPIcs.FSTTCS.2018.37⟩ |
| DOI: | 10.4230/LIPIcs.FSTTCS.2018.37⟩ |
| Popis: | International audience; We introduce a dependent-type theory ∆-framework, LF-∆ , based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives intersection, union, and relevant implication. Proof-functional connectives take into account the shape of logical proofs, thus allowing the user to reflect polymorphic features of proofs in formulae. This is in contrast to classical and intuitionistic connectives where the meaning of a compound formula is dependent only on the truth value or the provability of its subformulae. Both Logical Frameworks and Proof Functional Logics consider proofs as first class citizens albeit differently. The former mention proofs explicitly, while the latter mention proofs implicitly. Their combination therefore opens up new possibilites of formal reasoning on proof-theoretic semantics. We study the metatheory of LF-∆ and provide various examples of applications. Moreover, we discuss a prototype implementation of a type checker and a refiner allowing the user to accelerate and possibly automate, the proof development process. This proof-functional type theory can be plugged in existing common proof assistants. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|