Towards explicit rewrite rules in the λΠ-calculus modulo

Abstract : This paper provides a new presentation of the λΠ-calculus modulo where the addition of rewrite rules is made explicit. The λΠ-calculus modulo is a variant of the λ-calculus with dependent types where β-reduction is extended with user-defined rewrite rules. Its expressiveness makes it suitable to serve as an output language for theorem provers, certified development tools or proof assistants. Addition of rewrite rules becomes an iterative process and rules previously added can be used to type new rules. We also discuss the condition rewrite rules must satisfy in order to preserve the Subject Reduction property and we give a criterion weaker than the usual one. Finally we describe the new version of Dedukti, a type-checker for the λΠ-calculus modulo for which we assess its efficiency in comparison with Coq, Twelf and Maude.
Type de document :
Communication dans un congrès
IWIL - 10th International Workshop on the Implementation of Logics, Dec 2013, Stellenbosch, South Africa. 2013
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00921340
Contributeur : Ronan Saillard <>
Soumis le : mardi 14 janvier 2014 - 10:15:37
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 15 avril 2014 - 16:21:25

Fichier

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

Identifiants

  • HAL Id : hal-00921340, version 2

Collections

Citation

Ronan Saillard. Towards explicit rewrite rules in the λΠ-calculus modulo. IWIL - 10th International Workshop on the Implementation of Logics, Dec 2013, Stellenbosch, South Africa. 2013. 〈hal-00921340v2〉

Partager

Métriques

Consultations de la notice

415

Téléchargements de fichiers

198