swMATH27482MaRDI QIDQ39198FDOQ39198
Author name not available (Why is that?)
Official website: http://oeuf.uwplse.org/
Source code repository: https://github.com/uwplse/oeuf
Cited In (15)
- Proof-producing synthesis of CakeML from monadic HOL functions
- The \textsc{MetaCoq} project
- CakeML
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- CertiCoq
- gMark
- Template-Coq
- HOL Light QE
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- MetaCoq
- Extracting functional programs from Coq, in Coq
- Certified Graph View Maintenance with Regular Datalog
- A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
- coq-library-undecidability
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for software: OEuf
