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-6zbMATH Open1356.68186OpenAlexW1904308182MaRDI QIDQ286790FDOQ286790
Authors: 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
Recommendations
Cites Work
- A Brief Overview of HOL4
- Edinburgh LCF. A mechanized logic of computation
- Title not available (Why is that?)
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Unified QBF certification and its applications
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- An axiomatic basis for computer programming
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- 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
- 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
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0
- Towards Self-verification of HOL Light
- Title not available (Why is that?)
- 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
- Linear and nonlinear arithmetic in ACL2
- Formalization and implementation of modern SAT solvers
- Rewriting with equivalence relations in ACL2
Cited In (11)
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- A verified generational garbage collector for CakeML
- Formalization of the resolution calculus for first-order logic
- A verified proof checker for higher-order logic
- HOL Zero’s Solutions for Pollack-Inconsistency
- Milawa
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- A verified runtime for a verified theorem prover
- 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
Uses Software
This page was built for publication: The reflective Milawa theorem prover is sound (down to the machine code that runs it)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286790)
