CertiCoq
From MaRDI portal
Software:34519
No author found.
Related Items (17)
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 ⋮ Translation certification for smart contracts ⋮ Extracting functional programs from Coq, in Coq ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ The \textsc{MetaCoq} project ⋮ Verified Characteristic Formulae for CakeML ⋮ [https://portal.mardi4nfdi.de/wiki/Publication:5875425 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 ⋮ 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 ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem
This page was built for software: CertiCoq
