A verified theorem prover backend supported by a monotonic library

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • Luxembourg University, Luxembourg
  • Cornell University

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.

Details

Original languageEnglish
Title of host publicationLPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
EditorsGilles Barthe, Geoff Sutcliffe, Margus Veanes
Publication statusPublished - 23 Oct 2018
EventLPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Awassa, Ethiopia
Duration: 17 Nov 201821 Nov 2018

Publication series

NameEPiC Series in Computing
PublisherEasyChair Publications
Volume57
ISSN (Electronic)2398-7340

Conference

ConferenceLPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
CountryEthiopia
CityAwassa
Period17/11/1821/11/18

Keywords

  • Coq, Digital Library, Kripke semantics, monotonicity, Nuprl, proof checker, Verified theorem prover backend