The ∆-framework

Furio Honsell 1 Luigi Liquori 2, 3 Claude Stolze 2 Ivan Scagnetto 1
2 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : 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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01701934
Contributeur : Luigi Liquori <>
Soumis le : lundi 22 juillet 2019 - 16:45:40
Dernière modification le : mardi 23 juillet 2019 - 13:33:30

Fichier

Delta-framework.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

Citation

Furio Honsell, Luigi Liquori, Claude Stolze, Ivan Scagnetto. The ∆-framework. 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⟩. ⟨hal-01701934v2⟩

Partager

Métriques

Consultations de la notice

109

Téléchargements de fichiers

24