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

DOI10.1007/978-3-319-94205-6_42zbMATH Open1468.68060OpenAlexW2810040629MaRDI QIDQ1799129FDOQ1799129

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

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

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)

Cited In (8)

• Proof-producing synthesis of CakeML from monadic HOL functions
• A verified compiler from Isabelle/HOL to CakeML
• Characteristic formulae for liveness properties of non-terminating CakeML programs
• A verified proof checker for higher-order logic
• 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

Uses Software

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

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)