Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                          Lundi 25 octobre, 10h30

                              ---------------
                              Matthieu Sozeau
                              ---------------

                                   INRIA

              ================================================
              Equations: A Dependent Pattern-Matching Compiler
              ================================================

We present a compiler for definitions by pattern matching on
inductive families in the Coq system. It permits 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.