OEuf
From MaRDI portal
Software:39198
swMATH27482MaRDI QIDQ39198FDOQ39198
Author name not available (Why is that?)
Source code repository: https://github.com/uwplse/oeuf
Cited In (8)
- Proof-producing synthesis of CakeML from monadic HOL functions
- The \textsc{MetaCoq} project
- 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
- 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
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for software: OEuf
