The reflective Milawa theorem prover is sound (down to the machine code that runs it)
From MaRDI portal
Publication:286790
DOI10.1007/s10817-015-9324-6zbMath1356.68186OpenAlexW1904308182MaRDI QIDQ286790
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
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)
