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

DOI10.1017/S0956796813000282MaRDI QIDQ2875232zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Proof-producing synthesis of ML from higher-order logic
• Proof-producing synthesis of CakeML from monadic HOL functions
• scientific article; zbMATH DE number 2003148
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• A verified compiler from Isabelle/HOL to CakeML

Cites work

• A formally verified compiler back-end
• A Thread of HOL Development
• 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

(22)

• Adapting functional programs to higher order logic
• TWAM: a certifying abstract machine for logic programs
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• Proof-producing synthesis of CakeML from monadic HOL functions
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Proof-producing reflection for HOL. With an application to model polymorphism
• Pattern matches in HOL: a new representation and improved code generation
• Verified characteristic formulae for CakeML
• Automatically Translating Type and Function Definitions from HOL to ACL2
• Compilation as Rewriting in Higher Order Logic
• The verified CakeML compiler backend
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code
• Trustworthy Graph Algorithms (Invited Talk)
• Proof-producing synthesis of ML from higher-order logic
• Trusted Source Translation of a Total Function Language
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Efficient verified (UN)SAT certificate checking
• Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
• Candle: a verified implementation of HOL Light (extended version)
• A mechanised semantics for HOL with ad-hoc overloading
• Certified MaxSAT preprocessing

Describes a project that uses

Uses Software

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

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)