Cited in
(37)- Formally verifying the solution to the Boolean Pythagorean triples problem
- Translation certification for smart contracts
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- ANF preserves dependent types up to extensional equality
- Proof-producing synthesis of CakeML from monadic HOL functions
- A verified generational garbage collector for CakeML
- Extracting functional programs from Coq, in Coq
- A verified generational garbage collector for CakeML
- Fast machine words in Isabelle/HOL
- Verified characteristic formulae for CakeML
- CakeML
- CompCert
- Mtac
- HOL-TestGen
- HALO
- Pilsner
- Fiat
- CertiKOS
- TIL
- HoTTSQL
- Gallina
- OEuf
- Bedrock
- Template-Coq
- HOL Light QE
- Q*cert
- SEQUEL
- SQLCert
- MetaCoq
- A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- A Coq formalisation of SQL's execution engines
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Trace-relating compiler correctness and secure compilation
- coq-library-undecidability
- The \textsc{MetaCoq} project
- Towards certified meta-programming with typed Template-Coq
This page was built for software: CertiCoq
