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

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
• Proof-Producing Reflection for HOL
• 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
• A Verified Theorem Prover Backend Supported by a Monotonic Library
• HOL Zero’s Solutions for Pollack-Inconsistency
• Proof-producing synthesis of ML from higher-order logic
• 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
• 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
• Towards a Formally Verified Proof Assistant
• A Verified Runtime for a Verified Theorem Prover
• A consistent foundation for Isabelle/HOL

This page was built for software: Milawa