The following pages link to CakeML (Q20799):
Displayed 50 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)
- Introduction to ``Milestones in interactive theorem proving'' (Q1663212) (← 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)
- Verified spilling and translation validation with repair (Q1687761) (← links)
- Verifying the LTL to Büchi automata translation via very weak alternating automata (Q1791171) (← links)
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper) (Q1791178) (← links)
- Fast machine words in Isabelle/HOL (Q1791180) (← links)
- A formal equational theory for call-by-push-value (Q1791198) (← links)
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions (Q1799129) (← links)
- An abstraction-refinement framework for reasoning with large theories (Q1799131) (← 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)
- Hoare-style logic for unstructured programs (Q2038040) (← 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)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- Metamath Zero: designing a theorem prover prover (Q2219381) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- A verified compiler from Isabelle/HOL to CakeML (Q2324018) (← links)
- Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (Q2402234) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Lem (Q2819676) (← 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)
- Towards a Formally Verified Proof Assistant (Q2879241) (← links)
- HOL with Definitions: Semantics, Soundness, and a Verified Implementation (Q2879260) (← links)
- The Reflective Milawa Theorem Prover Is Sound (Q2879267) (← links)
- Improved Tool Support for Machine-Code Decompilation in HOL4 (Q2945632) (← links)
- Pattern Matches in HOL: (Q2945657) (← links)
- Refinement through restraint: bringing down the cost of verification (Q2982005) (← links)
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- Computational logic: its origins and applications (Q4559535) (← links)
- The verified CakeML compiler backend (Q4972072) (← links)
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (Q5048997) (← links)
- (Q5094131) (← 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)
- Verified secure compilation for mixed-sensitivity concurrent programs (Q5152660) (← links)