Equations: A Dependent Pattern-Matching Compiler

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 as a set of equations, automatically find their realization in the core type theory and generate proofs to ease reasoning on them. It provides a complete package to define and reason on functions in the proof assistant, substantially reducing the boilerplate code and proofs one usually has to write, also hiding the in- tricacies related to the use of dependent types and complex recursion schemes.
Type de document :
Article dans une revue
Lecture Notes in Computer Science, Springer, 2010, 6172, 〈10.1007/978-3-642-14052-5_29〉
Liste complète des métadonnées

Contributeur : Matthieu Sozeau <>
Soumis le : mardi 4 octobre 2011 - 13:47:35
Dernière modification le : mardi 8 janvier 2019 - 09:22:02



Matthieu Sozeau. Equations: A Dependent Pattern-Matching Compiler. Lecture Notes in Computer Science, Springer, 2010, 6172, 〈10.1007/978-3-642-14052-5_29〉. 〈inria-00628862〉



Consultations de la notice