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

Thomas Powell

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 t…