CakeML
From MaRDI portal
Cited in
(only showing first 100 items - show all)- FRAT
- cake_lpr
- SBSAT
- CoqEAL
- Algolib
- Introduction to ``Milestones in interactive theorem proving
- 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
- Verified spilling and translation validation with repair
- LLVM
- HOL
- Verifying the LTL to Büchi automata translation via very weak alternating automata
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Fast machine words in Isabelle/HOL
- A formal equational theory for call-by-push-value
- Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
- An abstraction-refinement framework for reasoning with large theories
- PIDE
- HOL Light
- A verified proof checker for higher-order logic
- Foreword to the special focus on formal proofs for mathematics and computer science
- CompCertTSO
- CoCon: a conference management system with formally verified document confidentiality
- Hoare-style logic for unstructured programs
- versat
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- Lem
- A formal semantics of the GraalVM intermediate representation
- Translation certification for smart contracts
- CompCert
- Coquet
- Milawa
- Gmeta
- LNgen
- Proof-producing synthesis of CakeML from monadic HOL functions
- Metamath Zero: designing a theorem prover prover
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- From LCF to Isabelle/HOL
- Paco
- GRUNGE: a grand unified ATP challenge
- A verified compiler from Isabelle/HOL to CakeML
- Poly/ML
- Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings
- Autoref
- Jitawa
- GDSL
- ConfiChair
- Vellvm
- libclang
- MLton
- seL4
- A higher-order abstract syntax approach to verified transformations on functional programs
- Lem: reusable engineering of real-world semantics
- CoSMed: a confidentiality-verified social media platform
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- Jif
- 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
- Towards a formally verified proof assistant
- HOL with definitions: semantics, soundness, and a verified implementation
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Haskabelle
- CoSMed
- Ur/Web
- HOL Zero
- Improved tool support for machine-code decompilation in HOL4
- Pattern matches in HOL: a new representation and improved code generation
- Refinement through restraint: bringing down the cost of verification
- Verified characteristic formulae for CakeML
- ARMor
- Cogent
- Pilsner
- MiniAgda
- Fiat
- GRAT
- Autosubst
- CompCertS
- LVC
- CertiCoq
- HALO
- OEuf
- Template-Coq
- VST-Floyd
- Rust
- PairingHeap
- Splay Tree
- Skew Heap
- Bedrock
- Jinja Threads
- Edmonds-Karp
- Tame Graphs
- BicolanoMT
- Lava
- muFP
- Dictionary Construction
- Affine Arithmetic
- CAVA LTL Modelchecker
This page was built for software: CakeML
