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

Thomas Powell. Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language. Logical Methods in Computer Science, 20(1), 2024. [doi]

Abstract

Abstract is missing.