Proof-producing translation of higher-order logic into pure and stateful ML
From MaRDI portal
Publication:2875232
Recommendations
Cites work
- A Thread of HOL Development
- A formally verified compiler back-end
- Adapting functional programs to higher order logic
- Proof producing synthesis of arithmetic and cryptographic hardware
- Proving Theorems about LISP Functions
- The calculus of constructions
- Verification of the Miller-Rabin probabilistic primality test.
Cited in
(18)- Adapting functional programs to higher order logic
- The verified CakeML compiler backend
- Proof-producing synthesis of ML from higher-order logic
- Pattern matches in HOL: a new representation and improved code generation
- Proof-producing synthesis of CakeML from monadic HOL functions
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- TWAM: a certifying abstract machine for logic programs
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- Verified characteristic formulae for CakeML
- Automatically Translating Type and Function Definitions from HOL to ACL2
- Proof-producing reflection for HOL. With an application to model polymorphism
- Efficient verified (UN)SAT certificate checking
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- Compilation as Rewriting in Higher Order Logic
- Trusted Source Translation of a Total Function Language
- Trustworthy Graph Algorithms (Invited Talk)
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for publication: Proof-producing translation of higher-order logic into pure and stateful ML
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2875232)
