Full reduction at full throttle

Abstract : Emerging trends in proof styles and new applications of interactive proof assistants exploit the computational facilities of the provided proof language, reaping enormous benefits in proof size and convenience to the user. However, the resulting proof objects really put the proof assistant to the test in terms of computational time required to check them. We present a novel translation of the terms of the full Calculus of (Co)Inductive Constructions to OCAML programs. Building on this translation, we further present a new fully featured version of COQ that offloads much of the computation required during proof checking to a vanilla, state of the art and fine tuned compiler. This modular scheme yields substantial performance improvements over existing systems at a reduced implementation cost. The work presented here builds on previous work described in [GL02], but we place particular emphasis in this paper on the fact that this scheme is in fact an instance of untyped normalization by evaluation [FR04, Lin05, AHN08, Boe10].
Type de document :
Communication dans un congrès
Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011, Certified Programs and Proofs. 〈10.1007/978-3-642-25379-9_26〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00650940
Contributeur : Maxime Dénès <>
Soumis le : lundi 12 décembre 2011 - 15:03:21
Dernière modification le : jeudi 11 janvier 2018 - 16:22:52
Document(s) archivé(s) le : mardi 13 mars 2012 - 02:30:40

Fichiers

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

Identifiants

Collections

Citation

Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire. Full reduction at full throttle. Certified Programs and Proofs, Dec 2011, Kenting, Taiwan. 2011, Certified Programs and Proofs. 〈10.1007/978-3-642-25379-9_26〉. 〈hal-00650940〉

Partager

Métriques

Consultations de la notice

846

Téléchargements de fichiers

478