Equations: A Dependent Pattern-Matching Compiler
From MaRDI portal
Publication:5747666
DOI10.1007/978-3-642-14052-5_29zbMath1291.68369OpenAlexW1570978294MaRDI QIDQ5747666
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_29
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Foundations of dependent interoperability ⋮ A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Eliminating dependent pattern matching without K ⋮ Ornaments for Proof Reuse in Coq ⋮ Mechanically certifying formula-based Noetherian induction reasoning
Uses Software
This page was built for publication: Equations: A Dependent Pattern-Matching Compiler
