A Framework for Proof-carrying Logical Transformations

Quentin Garchery

In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this paper, we develop a framework to improve confidence in their results. We follow a modular and skeptical approach: transformations are instrumented independently of each other and produce certificates that are checked by a third-party tool. Logical transformations are considered in a higher-order logic, with type polymorphism and built-in theories such as equality and integer arithmetic. We develop a language of proof certificates for them and use it to implement the full chain of certificate generation and certificate verification.

In Chantal Keller and Mathias Fleury: Proceedings Seventh Workshop on Proof eXchange for Theorem Proving (PxTP 2021), Pittsburg, USA, 11th July 2021, Electronic Proceedings in Theoretical Computer Science 336, pp. 5–23.
Published: 7th July 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.336.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org