CakeML

swMATH8799MaRDI QIDQ20799FDOQ20799

Author name not available (Why is that?)

Cited In (59)

• Proof-producing synthesis of CakeML from monadic HOL functions
• CoCon: a conference management system with formally verified document confidentiality
• Metamath Zero: designing a theorem prover prover
• Title not available (Why is that?)
• A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
• Lem: reusable engineering of real-world semantics
• The Reflective Milawa Theorem Prover Is Sound
• Operational semantics of a weak memory model with channel synchronization
• Title not available (Why is that?)
• Efficient verified (UN)SAT certificate checking
• CakeML
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Fast machine words in Isabelle/HOL
• Foreword to the special focus on formal proofs for mathematics and computer science
• Verifying the LTL to Büchi automata translation via very weak alternating automata
• A verified compiler from Isabelle/HOL to CakeML
• A verified proof checker for higher-order logic
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9
• POPLMark reloaded: Mechanizing proofs by logical relations
• Refinement through restraint: bringing down the cost of verification
• Pattern Matches in HOL:
• Hoare-style logic for unstructured programs
• Verified Characteristic Formulae for CakeML
• A formal semantics of the GraalVM intermediate representation
• Title not available (Why is that?)
• A verified ODE solver and the Lorenz attractor
• CoSMed: a confidentiality-verified social media platform
• Introduction to ``Milestones in interactive theorem proving
• Mechanising a type-safe model of multithreaded Java with a verified compiler
• Proof Auditing Formalised Mathematics
• GRUNGE: a grand unified ATP challenge
• Translation certification for smart contracts
• A formal equational theory for call-by-push-value
• Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
• Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The verified CakeML compiler backend
• Improved Tool Support for Machine-Code Decompilation in HOL4
• An abstraction-refinement framework for reasoning with large theories
• Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
• Isabelle's metalogic: formalization and proof checker
• A verified generational garbage collector for CakeML
• A formalization and proof checker for Isabelle's metalogic
• A Framework for the Automatic Formal Verification of Refinement from Cogent to C
• From LCF to Isabelle/HOL
• Extracting functional programs from Coq, in Coq
• The CADE-26 automated theorem proving system competition – CASC-26
• Computational logic: its origins and applications
• Schulze voting as evidence carrying computation
• Verified spilling and translation validation with repair
• CoSMed: A Confidentiality-Verified Social Media Platform
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Towards a Formally Verified Proof Assistant
• Amortized complexity verified
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A verified generational garbage collector for CakeML
• Verified secure compilation for mixed-sensitivity concurrent programs
• Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs

This page was built for software: CakeML