The λΠ-calculus Modulo as a Universal Proof Language

Abstract : The λΠ -calculus forms one of the vertices in Barendregt's -cube and has been used as the core language for a number of logical frameworks. Following earlier extensions of natural deduction, Cousineau and Dowek generalize the de nitional equality of this well studied calculus to an arbitrary congruence generated by rewrite rules, which allows for more faithful encodings of foreign logics. This paper motivates the resulting language, the λΠ -calculus modulo, as a universal proof language, capable of expressing proofs from many other systems without losing their computational properties. We further show how to very simply and e ciently check proofs from this language. We have implemented this scheme in a proof checker called Dedukti.
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00917845
Contributeur : Claire Medrala <>
Soumis le : jeudi 12 décembre 2013 - 15:33:32
Dernière modification le : mercredi 27 mars 2019 - 16:41:26
Document(s) archivé(s) le : vendredi 14 mars 2014 - 11:20:39

Fichier

PxTP-Hermant-2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00917845, version 1

Collections

Citation

Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant. The λΠ-calculus Modulo as a Universal Proof Language. the Second International Workshop on Proof Exchange for Theorem Proving (PxTP 2012), Jun 2012, Manchester, United Kingdom. pp. 28-43. ⟨hal-00917845⟩

Partager

Métriques

Consultations de la notice

961

Téléchargements de fichiers

224