Metaprogramming and Dependent Types

Vincent Archambault

We explore the idea of using Coq formal language (Gallina) as its own metalanguage in the same way Scheme is its own metalanguage. This entails both the possibility of using Gallina as a replacement for Ltac and to use Gallina to define and prove properties about new syntactic forms. We investigate what modifications must be done to Gallina and the Coq ecosystem in order to achieve the above goal and discuss some technical results.