Towards a Logical Framework with Intersection and Union Types

Claude Stolze 1 Luigi Liquori 1 Furio Honsell 2 Ivan Scagnetto 2
1 CRISAM - Inria Sophia Antipolis - Méditerranée
2 DIMI - Dipartimento di Matematica e Informatica - Universita Udine
Abstract : We present an ongoing implementation of a dependent-type theory (∆-framework) based on the Edinburgh Logical Framework LF, extended with Proof-functional logical connectives such as intersection , union, and strong (or minimal relevant) implication. Proof-functional connectives take into account the shape of logical proofs, thus allowing to reflect polymorphic features of proofs in formulae. This is in contrast to classical Truth-functional connec-tives where the meaning of a compound formula is only dependent on the truth value of its subformulas. Both Logical Frameworks and proof functional logics consider proofs as first class citizens. But they do it differently namely, explicitly in the former while implicitly in the latter. Their combination opens up new possibilites of formal reasoning on proof-theoretic semantics. We provide some examples in the extended type theory and we outline a type checker. The theory of the system is under investigation. Once validated in vitro, the proof-functional type theory can be successfully plugged in existing truth-functional proof assistants.
Type de document :
Communication dans un congrès
11th International Workshop on Logical Frameworks and Meta-languages, LFMTP, Sep 2017, Oxford, United Kingdom. pp.1 - 9, 2017
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01534035
Contributeur : Luigi Liquori <>
Soumis le : jeudi 12 octobre 2017 - 15:56:05
Dernière modification le : samedi 27 janvier 2018 - 01:31:23

Fichier

paper-sigconf.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01534035, version 2

Collections

INRIA2017 | INRIA

Citation

Claude Stolze, Luigi Liquori, Furio Honsell, Ivan Scagnetto. Towards a Logical Framework with Intersection and Union Types. 11th International Workshop on Logical Frameworks and Meta-languages, LFMTP, Sep 2017, Oxford, United Kingdom. pp.1 - 9, 2017. 〈hal-01534035v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

191

Téléchargements de fichiers

70

Contact


archive-ouverte@inria.fr