swMATH12812MaRDI QIDQ24736FDOQ24736
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/~mom22/jitawa/
Cited In (33)
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Aligning concepts across proof assistant libraries
- A verified generational garbage collector for CakeML
- Formalization of the resolution calculus for first-order logic
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Steps towards Verified Implementations of HOL Light
- A verified proof checker for higher-order logic
- ProofPower
- Polar
- CompCertTSO
- CakeML
- Milawa
- HOL Zero
- HOL Zero's solutions for Pollack-inconsistency
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- theoremprover-museum
- GCminor
- Abstract Soundness
- Knuth Bendix Orders
- Incompleteness Theorems
- Incredible Proof Machine
- Light-weight Containers
- Verified Prover
- FOL_Harrison
- DefunT
- OpenTheory
- TXDT
- Towards a formally verified proof assistant
- HOL with definitions: semantics, soundness, and a verified implementation
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Metamath Zero
- A formalization and proof checker for Isabelle's metalogic
- A consistent foundation for Isabelle/HOL
This page was built for software: Jitawa
