Equations: a dependent pattern-matching compiler

Matthieu Sozeau

Équipe pi.r2
Laboratoire Programmes, Preuves et Systèmes (PPS)
INRIA Paris - Rocquencourt

Thursday, 31 May 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: We present a compiler for definitions made by pattern matching on inductive families in the Coq system. It allows to write structured, recursive dependently-typed functions, automatically find their realization in the core type theory and generate proofs to ease reasoning on them. The high-level interface allows to write dependently-typed functions on inductive families in a style close to Agda or Epigram, while their low-level implementation is accepted by the vanilla core type theory of Coq. This setup uses the smallest trusted code base possible and additional tools are provided to maintain a high-level view of definitions. The compiler makes heavy use of type classes and the high-level tactic language of Coq for greater genericity and extensibility.

This talk is given in the frame of the 4th French month of science in Estonia.

IFE
Tarmo Uustalu
Last update 20.4.2012