Sites Inria

English version

Séminaire des équipes de recherche

Towards Certified Meta-Programming with Typed Template-Coq

I will present Template-Coq which is a Coq plugin to quote and unquote terms.

  • Date : 4/06/2018
  • Lieu : Inria de Paris, 2 rue Simone Iff, 75012 Paris, bâtiment C, salle J.L. Lions 2 - 2:00 pm
  • Intervenant(s) : Simon Boulier (Inria Nantes)

In this plugin, a reification of the syntax is provided together with functions to move from terms to syntax and back. Recently we extended Template-Coq in two ways:

  • reification of typing which open the way to implement certified tools manipulating Coq terms (including a type checker!)
  • reification of commands through a monad, opening the way to implement Coq plugins directly in Coq (I will show such examples)

This talk will be a presentation of this paper, accepted at ITP 2018:


Mots-clés : Séminaire Prosecco Equipe de recherche Inria de Paris

Haut de page

Suivez Inria