Proof-producing translation of higher-order logic into pure and stateful ML

DOI10.1017/S0956796813000282zbMath1297.68053OpenAlexW1969704856MaRDI QIDQ2875232

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (12)

Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ TWAM: a certifying abstract machine for logic programs ⋮ Proof-Producing Reflection for HOL ⋮ Pattern Matches in HOL: ⋮ Unnamed Item ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ Verified Characteristic Formulae for CakeML ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Efficient verified (UN)SAT certificate checking ⋮ The verified CakeML compiler backend ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code

Uses Software

• Coq
• ML
• Haskell
• HOL
• HOL Light
• CFML

Cites Work

• Adapting functional programs to higher order logic
• The calculus of constructions
• Verification of the Miller-Rabin probabilistic primality test.
• Proof producing synthesis of arithmetic and cryptographic hardware
• A formally verified compiler back-end
• Proving Theorems about LISP Functions
• A Thread of HOL Development

This page was built for publication: Proof-producing translation of higher-order logic into pure and stateful ML