A First-Order Representation of Pure Type Systems Using Superdeduction

Guillaume Burel 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Superdeduction is a formalism closely related to deduction modulo which permits to enrich a deduction system (especially a first-order one such as natural deduction or sequent calculus) with new inference rules automatically computed from the presentation of a theory. We give a natural encoding from every functional Pure Type System (PTS) into superdeduction by defining an appropriate first-order theory. We prove that this translation is correct and conservative, showing a correspondence between valid typing judgments in the PTS and provable sequents in the corresponding superdeductive system. As a byproduct, we also introduce the superdeductive sequent calculus for intuitionistic logic, which was until now only defined for classical logic. We show its equivalence with the superdeductive natural deduction. This implies that superdeduction can be easily used as a logical framework. These results lead to a better understanding of the implementation and the automation of proof search for PTS, as well as to more cooperation between proof assistants.
Type de document :
Communication dans un congrès
Frank Pfenning. 23rd Annual IEEE Symposium on Logic In Computer Science, Jun 2008, Pittsburgh, PA, United States. IEEE Computer Society, pp.253-263, 2008, Logic In Computer Science. 〈10.1109/LICS.2008.22〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00198543
Contributeur : Guillaume Burel <>
Soumis le : lundi 17 décembre 2007 - 15:23:43
Dernière modification le : jeudi 11 janvier 2018 - 01:49:21
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 11:35:53

Fichier

NJ_asLF.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Burel. A First-Order Representation of Pure Type Systems Using Superdeduction. Frank Pfenning. 23rd Annual IEEE Symposium on Logic In Computer Science, Jun 2008, Pittsburgh, PA, United States. IEEE Computer Society, pp.253-263, 2008, Logic In Computer Science. 〈10.1109/LICS.2008.22〉. 〈inria-00198543〉

Partager

Métriques

Consultations de la notice

166

Téléchargements de fichiers

90