Milawa

swMATH9977MaRDI QIDQ21954

No author found.

Described by source

• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• The Reflective Milawa Theorem Prover Is Sound

Related Items (18)

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 ⋮ Proof-Producing Reflection for HOL ⋮ A consistent foundation for Isabelle/HOL ⋮ A verified proof checker for higher-order logic ⋮ Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings ⋮ Proof-producing synthesis of ML from higher-order logic ⋮ A verified generational garbage collector for CakeML ⋮ Milestones from the Pure Lisp Theorem Prover to ACL2 ⋮ A verified generational garbage collector for CakeML ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ A Verified Theorem Prover Backend Supported by a Monotonic Library ⋮ 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

This page was built for software: Milawa