Milawa

swMATH9977MaRDI QIDQ21954FDOQ21954

Author name not available (Why is that?)

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 (down to the machine code that runs it)

Cited In (18)

• 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
• Proof-producing synthesis of ML from higher-order logic
• HOL Zero's solutions for Pollack-inconsistency
• A verified runtime for a verified theorem prover
• Towards a formally verified proof assistant
• Milestones from the Pure Lisp Theorem Prover to ACL2
• A verified generational garbage collector for CakeML
• A formalization and proof checker for Isabelle's metalogic
• A verified theorem prover backend supported by a monotonic library
• 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
• A consistent foundation for Isabelle/HOL
• Proof-producing reflection for HOL. With an application to model polymorphism

This page was built for software: Milawa