Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language

TL;DR

This paper introduces a logic that combines first-order reasoning with stateful program semantics, enabling extraction of sequential programs from logical proofs via an interpretation into an imperative language.

Contribution

It presents a novel extension of first-order logic with Hoare-style assertions and provides a realizability interpretation that extracts sequential programs acting on state.

Findings

Programs act on state sequentially

Logic can be instantiated for various extensions

Interpretation uses state monad for semantics

Abstract

We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizability interpretation of our logic that extracts programs into a mixed functional/imperative language. All programs expressible in this language act on the state in a sequential manner, and we make this intuition precise by interpreting them in a semantic metatheory using the state monad. Our basic framework is very general, and our intention is that it can be instantiated and extended in a variety of different ways. We outline in detail one such extension: A monadic version of Heyting arithmetic with a wellfounded while rule, and conclude by outlining several other directions for future work.