Towards Certified Meta-Programming with Typed Template-Coq

Abhishek Anand 1 Simon Boulier 2 Cyril Cohen 3 Matthieu Sozeau 4 Nicolas Tabareau 2
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
3 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
4 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
Abstract : Template-Coq is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declarations , as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq's AST in Gallina. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties, and to extract Coq terms to a CBV λ-calculus. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq's type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Calculus of Inductive Constructions (CIC), as implemented by Coq, including the kernel's declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq's logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of Template-Coq as a foundation for higher-level tools.
Type de document :
Communication dans un congrès
ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. Springer, 10895, pp.20-39, 2018, LNCS. 〈10.1007/978-3-319-94821-8_2〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger
Contributeur : Simon Boulier <>
Soumis le : jeudi 7 juin 2018 - 08:46:53
Dernière modification le : jeudi 15 novembre 2018 - 20:27:45
Document(s) archivé(s) le : samedi 8 septembre 2018 - 12:34:07


Fichiers produits par l'(les) auteur(s)



Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau. Towards Certified Meta-Programming with Typed Template-Coq. ITP 2018 - 9th Conference on Interactive Theorem Proving, Jul 2018, Oxford, United Kingdom. Springer, 10895, pp.20-39, 2018, LNCS. 〈10.1007/978-3-319-94821-8_2〉. 〈hal-01809681〉



Consultations de la notice


Téléchargements de fichiers