Typed Template Coq -- Certified Meta-Programming in Coq

Abhishek Anand 1 Simon Boulier 2 Nicolas Tabareau 2 Matthieu Sozeau 3
2 GALLINETTE - GALLINETTE
LS2N - Laboratoire des Sciences du Numérique de Nantes, Inria Rennes – Bretagne Atlantique
3 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, its use was extended for the needs of the CertiCoq certified compiler project, which uses it as its front-end language and to derive parametricity properties, and the work of Forster on extracting Coq terms to a CBV λ-calculus. However, the syntax currently lacks semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq itself. This is an issue for CertiCoq where both a non-deterministic small step semantics and a deterministic call-by-value big step semantics had to be defined and preserved, without an " official " reference specification to refer to. Our hope with this work is to remedy this situation and provide a formal semantics of Coq's implemented type theory, that can independently be refined and studied. By implementing a (partial) independent checker in Coq, we can also help formalize certified translations from Coq to Coq.
Type de document :
Communication dans un congrès
CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles, CA, United States. pp.1-2
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01671948
Contributeur : Matthieu Sozeau <>
Soumis le : vendredi 22 décembre 2017 - 17:42:56
Dernière modification le : mardi 19 juin 2018 - 01:19:49

Fichier

Anand-Boulier-Tabareau-Sozeau-...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01671948, version 1

Citation

Abhishek Anand, Simon Boulier, Nicolas Tabareau, Matthieu Sozeau. Typed Template Coq -- Certified Meta-Programming in Coq. CoqPL 2018 - The Fourth International Workshop on Coq for Programming Languages, Jan 2018, Los Angeles, CA, United States. pp.1-2. 〈hal-01671948〉

Partager

Métriques

Consultations de la notice

658

Téléchargements de fichiers

84