The reflective Milawa theorem prover is sound (down to the machine code that runs it)

DOI10.1007/s10817-015-9324-6zbMath1356.68186OpenAlexW1904308182MaRDI QIDQ286790

Jared Davis, Magnus O. Myreen

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9324-6

zbMATH Keywords

theorem provingsoundnessproof assistantmachine code

Mathematics Subject Classification ID

Related Items (9)

Formalization of the resolution calculus for first-order logic ⋮ A verified proof checker for 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 ⋮ Milawa ⋮ 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

Uses Software

• ACL2
• Coq
• Isabelle
• Isabelle/HOL
• z3
• HOL
• HOL Light
• NQTHM
• CakeML
• Ivy
• Jitawa
• DRAT-trim
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Formalization and implementation of modern SAT solvers
• Rewriting with equivalence relations in ACL2
• Integrating external deduction tools with ACL2
• Efficiently checking propositional refutations in HOL theorem provers
• Partial functions in ACL2
• Structured theory development for a mechanized logic
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Unified QBF certification and its applications
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Inprocessing Rules
• A Verified Runtime for a Verified Theorem Prover
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• HOL Light: An Overview
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0
• A Brief Overview of HOL4
• Towards Self-verification of HOL Light
• Metamathematics, Machines and Gödel's Proof
• Automated Testing and Debugging of SAT and QBF Solvers
• Verified just-in-time compiler on x86
• The challenge of computer mathematics
• Steps towards Verified Implementations of HOL Light
• CakeML
• Meta Reasoning in ACL2
• Theorem Proving in Higher Order Logics
• An axiomatic basis for computer programming
• Correct Hardware Design and Verification Methods

This page was built for publication: The reflective Milawa theorem prover is sound (down to the machine code that runs it)