Proof-producing translation of higher-order logic into pure and stateful ML
From MaRDI portal
Publication:2875232
DOI10.1017/S0956796813000282zbMATH Open1297.68053OpenAlexW1969704856MaRDI QIDQ2875232FDOQ2875232
Authors: Magnus O. Myreen, Scott Owens 
Publication date: 14 August 2014
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796813000282
Recommendations
Cites Work
- The calculus of constructions
- Proving Theorems about LISP Functions
- A formally verified compiler back-end
- Verification of the Miller-Rabin probabilistic primality test.
- Adapting functional programs to higher order logic
- Proof producing synthesis of arithmetic and cryptographic hardware
- A Thread of HOL Development
Cited In (17)
- Proof-producing synthesis of CakeML from monadic HOL functions
- Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
- Adapting functional programs to higher order logic
- Trusted Source Translation of a Total Function Language
- Efficient verified (UN)SAT certificate checking
- Proof-Producing Reflection for HOL
- TWAM: a certifying abstract machine for logic programs
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Pattern Matches in HOL:
- Verified Characteristic Formulae for CakeML
- Automatically Translating Type and Function Definitions from HOL to ACL2
- Trustworthy Graph Algorithms (Invited Talk)
- Title not available (Why is that?)
- Proof-producing synthesis of ML from higher-order logic
- The verified CakeML compiler backend
- Compilation as Rewriting in Higher Order Logic
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
Uses Software
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)
