Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}

DOI10.1007/978-3-319-94821-8_17OpenAlexW2811016949MaRDI QIDQ1791170

Andres Erbsen, Jason Gross, Adam Chlipala

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_17

Mathematics Subject Classification ID

Related Items (1)

The \textsc{MetaCoq} project

Uses Software

• Coq
• OCaml
• Template-Coq

This page was built for publication: Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}