Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Matthieu Sozeau Connect in order to contact the contributor
Submitted on : Tuesday, October 4, 2011 - 1:47:35 PM
Last modification on : Thursday, September 2, 2021 - 1:50:01 PM

Links full text



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⟩



Record views