CakeML
From MaRDI portal
Software:20799
No author found.
Related Items (59)
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 ⋮ Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ A formal semantics of the GraalVM intermediate representation ⋮ Computational logic: its origins and applications ⋮ Unnamed Item ⋮ Translation certification for smart contracts ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ 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 ⋮ Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings ⋮ Unnamed Item ⋮ 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 ⋮ Verified spilling and translation validation with repair ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Proof-producing synthesis of CakeML from monadic HOL functions ⋮ Refinement through restraint: bringing down the cost of verification ⋮ Metamath Zero: designing a theorem prover prover ⋮ 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 ⋮ Lem ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Amortized complexity verified ⋮ Verified secure compilation for mixed-sensitivity concurrent programs ⋮ A verified proof checker for higher-order logic ⋮ Foreword to the special focus on formal proofs for mathematics and computer science ⋮ A verified generational garbage collector for CakeML ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ CoCon: a conference management system with formally verified document confidentiality ⋮ A verified generational garbage collector for CakeML ⋮ Verifying the LTL to Büchi automata translation via very weak alternating automata ⋮ Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) ⋮ Fast machine words in Isabelle/HOL ⋮ A formal equational theory for call-by-push-value ⋮ Hoare-style logic for unstructured programs ⋮ A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs ⋮ Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions ⋮ An abstraction-refinement framework for reasoning with large theories ⋮ Efficient verified (UN)SAT certificate checking ⋮ The verified CakeML compiler backend ⋮ Isabelle's metalogic: formalization and proof checker ⋮ GRUNGE: a grand unified ATP challenge ⋮ A Verified Theorem Prover Backend Supported by a Monotonic Library ⋮ CoSMed: A Confidentiality-Verified Social Media Platform ⋮ A Framework for the Automatic Formal Verification of Refinement from Cogent to C ⋮ A verified compiler from Isabelle/HOL to CakeML ⋮ CakeML ⋮ Proof Auditing Formalised Mathematics ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Towards a Formally Verified Proof Assistant ⋮ HOL with Definitions: Semantics, Soundness, and a Verified Implementation ⋮ The Reflective Milawa Theorem Prover Is Sound
This page was built for software: CakeML
