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

https://hal.inria.fr/inria-00628862
Contributeur : Matthieu Sozeau <>
Soumis le : mardi 4 octobre 2011 - 13:47:35
Dernière modification le : mardi 4 octobre 2011 - 13:47:35

Identifiants

Citation

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〉

Partager

Métriques

Consultations de la notice

48