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