Pages that link to "Item:Q2875232"
From MaRDI portal
The following pages link to Proof-producing translation of higher-order logic into pure and stateful ML (Q2875232):
Displaying 12 items.
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- TWAM: a certifying abstract machine for logic programs (Q1629962) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- Proof-Producing Reflection for HOL (Q2945631) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- The verified CakeML compiler backend (Q4972072) (← links)
- Ready,<tt>Set</tt>, Verify! Applying<tt>hs-to-coq</tt>to real-world Haskell code (Q5018778) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- (Q5875431) (← links)
- Efficient verified (UN)SAT certificate checking (Q5919480) (← links)
