CakeML
From MaRDI portal
Cited in
(only showing first 100 items - show all)- 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
- The CADE-26 automated theorem proving system competition -- CASC-26
- Pattern matches in HOL: a new representation and improved code generation
- Lem: reusable engineering of real-world semantics
- Verified characteristic formulae for CakeML
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- A verified generational garbage collector for CakeML
- Operational semantics of a weak memory model with channel synchronization
- CakeML
- Efficient verified (UN)SAT certificate checking
- Fast machine words in Isabelle/HOL
- Verifying the LTL to Büchi automata translation via very weak alternating automata
- Foreword to the special focus on formal proofs for mathematics and computer science
- 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
- SBSAT
- CoqEAL
- Algolib
- LLVM
- HOL
- PIDE
- HOL Light
- CompCertTSO
- versat
- Lem
- CompCert
- Coquet
- Milawa
- Gmeta
- LNgen
- Paco
- Poly/ML
- Autoref
- Jitawa
- GDSL
- ConfiChair
- Vellvm
- libclang
- MLton
- seL4
- Jif
- Haskabelle
- CoSMed
- HOL Zero
- Ur/Web
- Cogent
- HALO
- ARMor
- Pilsner
- MiniAgda
- Fiat
- GRAT
- Autosubst
- CertiCoq
- CompCertS
- LVC
- OEuf
- Bedrock
- BicolanoMT
- Template-Coq
- Edmonds-Karp
- Affine Arithmetic
- Jinja Threads
- CAVA LTL Modelchecker
- PairingHeap
- Rust
- Dictionary Construction
- Lava
- muFP
- Skew Heap
- Haskell Show Class
- VST-Floyd
- Knuth Morris Pratt
- Splay Tree
- Tame Graphs
- CLDC
- Cloc
- JRIF
- IEEE_Floating_Point
- Polynomials
- IOzone
- OpenTheory
- GraalVM
- CakeML_Codegen
- Nominal2
- Metamath Zero
- FlowFox
- Coq-Combi
- Zeta_3_Irrational
- CoCon
- TSL
- MetaCoq
- A formal proof of the irrationality of \(\zeta(3)\)
This page was built for software: CakeML
