Jitawa
From MaRDI portal
Software:24736
swMATH12812MaRDI QIDQ24736FDOQ24736
Author name not available (Why is that?)
Cited In (14)
- 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
- HOL Zero’s Solutions for Pollack-Inconsistency
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Milestones from the Pure Lisp Theorem Prover to ACL2
- A formalization and proof checker for Isabelle's metalogic
- HOL with Definitions: Semantics, Soundness, and a Verified Implementation
- Towards a Formally Verified Proof Assistant
- A consistent foundation for Isabelle/HOL
This page was built for software: Jitawa
