CakeML
From MaRDI portal
swMATH8799MaRDI QIDQ20799FDOQ20799
Author name not available (Why is that?)
Official website: https://cakeml.org/
Cited In (only showing first 100 items - show all)
- CoCon: a conference management system with formally verified document confidentiality
- Metamath Zero: designing a theorem prover prover
- Lem: reusable engineering of real-world semantics
- Verified characteristic formulae for CakeML
- CakeML
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Fast machine words in Isabelle/HOL
- A verified compiler from Isabelle/HOL to CakeML
- A verified proof checker for higher-order logic
- A formal proof of the irrationality of \(\zeta(3)\)
- 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
- 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)
- 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
- Towards a formally verified proof assistant
- HOL with definitions: semantics, soundness, and a verified implementation
- Interactive theorem proving from the perspective of Isabelle/Isar
- GraalVM
- CakeML_Codegen
- Nominal2
- Metamath Zero
- FlowFox
- Coq-Combi
- Zeta_3_Irrational
- CoCon
- TSL
- MetaCoq
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- POPLMark reloaded: mechanizing proofs by logical relations
- FRAT
- cake_lpr
- Amortized complexity verified
- Proof-producing synthesis of CakeML from monadic HOL functions
- TBUDDY
- The CADE-26 automated theorem proving system competition -- CASC-26
This page was built for software: CakeML
