swMATH27569MaRDI QIDQ39285FDOQ39285
Author name not available (Why is that?)
Official website: https://link.springer.com/chapter/10.1007%2F978-3-319-94821-8_2
Cited In (13)
- The \textsc{MetaCoq} project
- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Mtac
- TCB
- Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac}
- CertiCoq
- Gallina
- OEuf
- HOL Light QE
- MetaCoq
- Extracting functional programs from Coq, in Coq
- A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
- coq-library-undecidability
This page was built for software: Template-Coq
