CertiCoq
From MaRDI portal
Software:34519
swMATH22728MaRDI QIDQ34519FDOQ34519
Author name not available (Why is that?)
Cited In (17)
- Proof-producing synthesis of CakeML from monadic HOL functions
- Formally verifying the solution to the Boolean Pythagorean triples problem
- The \textsc{MetaCoq} project
- A verified generational garbage collector for CakeML
- Fast machine words in Isabelle/HOL
- Trace-Relating Compiler Correctness and Secure Compilation
- Verified Characteristic Formulae for CakeML
- Translation certification for smart contracts
- A Coq formalisation of SQL's execution engines
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- 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
- A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
- Towards certified meta-programming with typed Template-Coq
This page was built for software: CertiCoq
