A Compiled Implementation of Strong Reduction

Benjamin Grégoire 1 Xavier Leroy 2
1 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : Motivated by applications to proof assistants based on dependent types, we develop and prove correct a strong reducer and β-equivalence checker for the λ-calculus with products, sums, and guarded fixpoints. Our approach is based on compilation to the bytecode of an abstract machine performing weak reductions on non-closed terms, derived with minimal modifications from the ZAM machine used in the Objective Caml bytecode interpreter, and complemented by a recursive "read back" procedure. An implementation in the Coq proof assistant demonstrates important speed-ups compared with the original interpreter-based implementation of strong reduction in Coq.
Type de document :
Communication dans un congrès
ICFP '02: seventh ACM SIGPLAN international conference on Functional programming , Oct 2002, Pittsburgh, United States. ACM, pp.235-246, 〈10.1145/581478.581501〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01499941
Contributeur : Xavier Leroy <>
Soumis le : samedi 1 avril 2017 - 17:38:55
Dernière modification le : vendredi 25 mai 2018 - 12:02:03
Document(s) archivé(s) le : dimanche 2 juillet 2017 - 12:40:16

Fichier

strong-reduction.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Benjamin Grégoire, Xavier Leroy. A Compiled Implementation of Strong Reduction. ICFP '02: seventh ACM SIGPLAN international conference on Functional programming , Oct 2002, Pittsburgh, United States. ACM, pp.235-246, 〈10.1145/581478.581501〉. 〈hal-01499941〉

Partager

Métriques

Consultations de la notice

305

Téléchargements de fichiers

48