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