CakeML
From MaRDI portal
Recommendations
- The verified CakeML compiler backend
- A verified generational garbage collector for CakeML
- A verified generational garbage collector for CakeML
- scientific article; zbMATH DE number 7699418
- scientific article; zbMATH DE number 6528605
- A verified compiler from Isabelle/HOL to CakeML
- PML2: integrated program verification in ML
- Verified characteristic formulae for CakeML
Cited in
(61)- TWAM: a certifying abstract machine for logic programs
- 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
- Schulze voting as evidence carrying computation
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- A verified proof checker for higher-order logic
- Foreword to the special focus on formal proofs for mathematics and computer science
- CoCon: a conference management system with formally verified document confidentiality
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- A formal semantics of the GraalVM intermediate representation
- Translation certification for smart contracts
- A better composition operator for quantitative information flow analyses
- Parameterized synthesis for fragments of first-order logic over data words
- Proof-producing synthesis of CakeML from monadic HOL functions
- From LCF to Isabelle/HOL
- GRUNGE: a grand unified ATP challenge
- A higher-order abstract syntax approach to verified transformations on functional programs
- CoSMed: a confidentiality-verified social media platform
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- 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
- Improved tool support for machine-code decompilation in HOL4
- Pattern matches in HOL: a new representation and improved code generation
- Verified characteristic formulae for CakeML
- A verified runtime for a verified theorem prover
- Computational logic: its origins and applications
- The verified CakeML compiler backend
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- Real-time MLton: a standard ML runtime for real-time functional programs
- Cogent: uniqueness types and certifying compilation
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
- Automatically Introducing Tail Recursion in CakeML
- Trustworthy Graph Algorithms (Invited Talk)
- Extracting functional programs from Coq, in Coq
- POPLMark reloaded: mechanizing proofs by logical relations
- The CADE-26 automated theorem proving system competition -- CASC-26
- The 9th IJCAR automated theorem proving system competition -- CASC-J9
- Highly automated formal proofs over memory usage of assembly code
- Proof auditing formalised mathematics
- scientific article; zbMATH DE number 7649970 (Why is no real title available?)
- scientific article; zbMATH DE number 7649976 (Why is no real title available?)
- Operational semantics of a weak memory model with channel synchronization
- Efficient verified (UN)SAT certificate checking
- A verified generational garbage collector for CakeML
- Grounding game semantics in categorical algebra
- Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
- Fast, verified computation for candle
- Amortized complexity verified
- Hoare-style logic for unstructured programs
- Correctly compiling proofs about programs without proving compilers correct
- Structured monads for generic first-order syntax metatheory
- Syntax monads for the working formal metatheorist
- A proof-producing compiler for blockchain applications
- Fast, verified computation for HOL ITPs
- A mechanised semantics for HOL with ad-hoc overloading
- Learning guided automated reasoning: a brief survey
- An empirical assessment of progress in automated theorem proving
- A mechanized first-order theory of algebraic data types with pattern matching
This page was built for publication: CakeML
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408415)
