Template-Coq

swMATH27569MaRDI QIDQ39285FDOQ39285

Author name not available (Why is that?)

Described by source

• Towards certified meta-programming with typed Template-Coq

Cited In (5)

• The \textsc{MetaCoq} project
• \texttt{slepice}: towards a verified implementation of type theory in type theory
• 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