Template-Coq

MaRDI QIDQ39285swMATHFDO

Official website https://link.springer.com/chapter/10.1007%2F978-3-319-94821-8_2

Described by source

• Towards certified meta-programming with typed Template-Coq

Cited in

(13)

• The \textsc{MetaCoq} project
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• Mtac
• TCB
• CertiCoq
• Gallina
• OEuf
• HOL Light QE
• MetaCoq
• coq-library-undecidability
• Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
• Extracting functional programs from Coq, in Coq
• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus

This page was built for software: Template-Coq