The following pages link to CakeML (Q5408415):
Displaying 44 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (Q287361) (← links)
- Amortized complexity verified (Q670702) (← links)
- TWAM: a certifying abstract machine for logic programs (Q1629962) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- CoSMed: a confidentiality-verified social media platform (Q1663221) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- Schulze voting as evidence carrying computation (Q1687758) (← links)
- A verified proof checker for higher-order logic (Q1987736) (← links)
- Foreword to the special focus on formal proofs for mathematics and computer science (Q2018656) (← links)
- CoCon: a conference management system with formally verified document confidentiality (Q2031419) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- A formal semantics of the GraalVM intermediate representation (Q2147184) (← links)
- Translation certification for smart contracts (Q2163161) (← links)
- A better composition operator for quantitative information flow analyses (Q2167722) (← links)
- Parameterized synthesis for fragments of first-order logic over data words (Q2200816) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- CoSMed: A Confidentiality-Verified Social Media Platform (Q2829248) (← links)
- A Framework for the Automatic Formal Verification of Refinement from Cogent to C (Q2829268) (← links)
- Improved Tool Support for Machine-Code Decompilation in HOL4 (Q2945632) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- The verified CakeML compiler backend (Q4972072) (← links)
- Ready,<tt>Set</tt>, Verify! Applying<tt>hs-to-coq</tt>to real-world Haskell code (Q5018778) (← links)
- Real-time MLton: A Standard ML runtime for real-time functional programs (Q5019014) (← links)
- Cogent: uniqueness types and certifying compilation (Q5019022) (← links)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (Q5048997) (← links)
- Automatically Introducing Tail Recursion in CakeML (Q5056071) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- Extracting functional programs from Coq, in Coq (Q5101927) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- The CADE-26 automated theorem proving system competition – CASC-26 (Q5145427) (← links)
- The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9 (Q5145447) (← links)
- Highly Automated Formal Proofs over Memory Usage of Assembly Code (Q5164171) (← links)
- Proof Auditing Formalised Mathematics (Q5195266) (← links)
- (Q5875430) (← links)
- (Q5875439) (← links)
- Operational semantics of a weak memory model with channel synchronization (Q5915975) (← links)
- Efficient verified (UN)SAT certificate checking (Q5919480) (← links)
