Cited in
(18)- \texttt{slepice}: towards a verified implementation of type theory in type theory
- Mtac
- TCB
- CertiKOS
- Autosubst
- CertiCoq
- HOLCF
- OEuf
- Template-Coq
- HOL Light QE
- Logipedia
- Metamath Zero
- PLM
- coq-library-undecidability
- Translation certification for smart contracts
- Extracting functional programs from Coq, in Coq
- Cubical Agda
- LogiKEy
This page was built for software: MetaCoq
