Jitawa
From MaRDI portal
Software:24736
No author found.
Related Items (14)
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 ⋮ Aligning concepts across proof assistant libraries ⋮ Formalization of the resolution calculus for first-order logic ⋮ Steps towards Verified Implementations of HOL Light ⋮ A consistent foundation for Isabelle/HOL ⋮ A verified proof checker for higher-order logic ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ A verified generational garbage collector for CakeML ⋮ HOL Zero’s Solutions for Pollack-Inconsistency ⋮ Verifying a concurrent garbage collector with a rely-guarantee methodology ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Towards a Formally Verified Proof Assistant ⋮ HOL with Definitions: Semantics, Soundness, and a Verified Implementation
This page was built for software: Jitawa
