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
