CakeML

DOI10.1145/2535838.2535841zbMath1284.68405OpenAlexW2006731094MaRDI QIDQ5408415

Ramana Kumar, Michael Norrish, Scott Owens, Magnus O. Myreen

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2535838.2535841

zbMATH Keywords

ML verified parsing compiler verification verified garbage collection compiler bootstrapping machine code verification read-eval-print loop verified type checking

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation ⋮ TWAM: a certifying abstract machine for logic programs ⋮ Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Automatically Introducing Tail Recursion in CakeML ⋮ A formal semantics of the GraalVM intermediate representation ⋮ Computational logic: its origins and applications ⋮ Translation certification for smart contracts ⋮ A verified ODE solver and the Lorenz attractor ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Mechanising a type-safe model of multithreaded Java with a verified compiler ⋮ A better composition operator for quantitative information flow analyses ⋮ Improved Tool Support for Machine-Code Decompilation in HOL4 ⋮ Pattern Matches in HOL: ⋮ Extracting functional programs from Coq, in Coq ⋮ Schulze voting as evidence carrying computation ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ Unnamed Item ⋮ Verified Characteristic Formulae for CakeML ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 ⋮ Amortized complexity verified ⋮ A verified proof checker for higher-order logic ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ From LCF to Isabelle/HOL ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Efficient verified (UN)SAT certificate checking ⋮ The verified CakeML compiler backend ⋮ Isabelle's metalogic: formalization and proof checker ⋮ GRUNGE: a grand unified ATP challenge ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ CoSMed: A Confidentiality-Verified Social Media Platform ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ Proof Auditing Formalised Mathematics ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code ⋮ Real-time MLton: A Standard ML runtime for real-time functional programs ⋮ Cogent: uniqueness types and certifying compilation ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software