Cited in
(15)- Proof-producing synthesis of CakeML from monadic HOL functions
- Extracting functional programs from Coq, in Coq
- CakeML
- CertiCoq
- gMark
- Template-Coq
- HOL Light QE
- 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
- Certified Graph View Maintenance with Regular Datalog
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- coq-library-undecidability
- The \textsc{MetaCoq} project
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for software: OEuf
