Verified Characteristic Formulae for CakeML

DOI10.1007/978-3-662-54434-1_22zbMath1485.68030OpenAlexW2596200388MaRDI QIDQ2988660

Armaël Guéneau, Magnus O. Myreen, Michael Norrish, Ramana Kumar

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_22

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Connecting Higher-Order Separation Logic to a First-Order Outside World ⋮ VST-Floyd: a separation logic tool to verify correctness of C programs ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ Characteristic formulae for liveness properties of non-terminating CakeML programs ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ A verified proof checker for higher-order logic ⋮ The verified CakeML compiler backend

Uses Software

• Coq
• Haskell
• OCaml
• HOL-Omega
• CakeML
• Toolchain
• seL4
• Fiat
• CertiCoq
• HALO
• Bedrock

Cites Work

• HALO
• Fiat
• Dependent types and multi-monadic effects in F*
• Proof-producing translation of higher-order logic into pure and stateful ML
• HALO
• Effective interactive proofs for higher-order imperative programs
• Self-certification
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
• Refinement to Imperative/HOL
• Refinement through restraint: bringing down the cost of verification
• Verified Software Toolchain
• The HOL-Omega Logic
• The verified CakeML compiler backend
• Program verification through characteristic formulae
• Characteristic formulae for the verification of imperative programs
• CakeML
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Verified Characteristic Formulae for CakeML