Equations: A Dependent Pattern-Matching Compiler

8 years 9 months ago
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 intricacies related to the use of dependent types and complex recursion schemes.
Matthieu Sozeau
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where ITP
Authors Matthieu Sozeau
Comments (0)