A Verified Theorem Prover Backend Supported by a Monotonic Library
Citations Over TimeTop 25% of 2018 papers
Abstract
Building a verified proof assistant entails implementing and mechanizing the concept of a library, as well as adding support for standard manipulations on it. In this work we develop such mechanism for the Nuprl proof assistant, and integrate it into the formalization of Nuprl’s meta-theory in Coq. We formally verify that standard operations on the library preserve its validity. This is a key property for any interactive theorem prover, since it ensures consistency. Some unique features of Nuprl, such as the presence of undefined abstractions, make the proof of this property nontrivial. Thus, e.g., to achieve monotonicity the semantics of sequents had to be refined. On a broader view, this work provides a backend for a verified version of Nuprl. We use it, in turn, to develop a tool that converts proofs exported from the Nuprl proof assistant into proofs in the Coq formalization of Nuprl’s meta-theory, so as to be verified.
Related Papers
- → How to make ad hoc proof automation less ad hoc(2011)30 cited
- → Machine Checking Proof Theory: An Application of Logic to Logic(2008)4 cited
- Parallelizing an interactive theorem prover: functional programming and proofs with acl2(2012)
- Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions(2007)