Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions

DOI10.1007/978-3-319-94205-6_42MaRDI QIDQ1799129zbMATH OpenOpenAlexFDO

Authors Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish, S. L. Ho

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_42

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Proof-producing synthesis of CakeML from monadic HOL functions
• A verified compiler from Isabelle/HOL to CakeML
• Proof-producing translation of higher-order logic into pure and stateful ML
• Proof-producing synthesis of ML from higher-order logic
• CakeML

Cited in

(8)

• Proof-producing synthesis of CakeML from monadic HOL functions
• A verified compiler from Isabelle/HOL to CakeML
• A verified proof checker for higher-order logic
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
• Proof-producing translation of higher-order logic into pure and stateful ML
• Synthesis of distributed mobile programs using monadic types in Coq
• A Hoare Logic for the State Monad

Describes a project that uses

Uses Software

• OEuf
• CertiCoq
• CakeML
• HOL
• Isabelle/HOL
• Coq

This page was built for publication: Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1799129)