CakeML

swMATH8799MaRDI QIDQ20799FDOQ20799

Author name not available (Why is that?)

Cited In (59)

• 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
• Proof-producing synthesis of CakeML from monadic HOL functions
• CoCon: a conference management system with formally verified document confidentiality
• The CADE-26 automated theorem proving system competition -- CASC-26
• Metamath Zero: designing a theorem prover prover
• Pattern matches in HOL: a new representation and improved code generation
• Lem: reusable engineering of real-world semantics
• Verified characteristic formulae for CakeML
• Operational semantics of a weak memory model with channel synchronization
• 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
• Improved tool support for machine-code decompilation in HOL4
• Refinement through restraint: bringing down the cost of verification
• Hoare-style logic for unstructured programs
• A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
• A formal semantics of the GraalVM intermediate representation
• A formal proof of the irrationality of \(\zeta(3)\)
• 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
• CoSMed: a confidentiality-verified social media platform
• 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 reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The verified CakeML compiler backend
• Towards a formally verified proof assistant
• HOL with definitions: semantics, soundness, and a verified implementation
• Interactive theorem proving from the perspective of Isabelle/Isar
• 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
• From LCF to Isabelle/HOL
• Extracting functional programs from Coq, in Coq
• A verified theorem prover backend supported by a monotonic library
• Computational logic: its origins and applications
• The 9th IJCAR automated theorem proving system competition -- CASC-J9
• POPLMark reloaded: mechanizing proofs by logical relations
• Schulze voting as evidence carrying computation
• Verified spilling and translation validation with repair
• A higher-order abstract syntax approach to verified transformations on functional programs
• Proof auditing formalised mathematics
• Amortized complexity verified
• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

This page was built for software: CakeML