Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
From MaRDI portal
Publication:6151555
DOI10.46298/lmcs-20(1:7)2024arXiv2301.01690v4OpenAlexW4391694971MaRDI QIDQ6151555
No author found.
Publication date: 11 March 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2301.01690v4
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Imperative programs as proofs via game semantics
- Toward the interpretation of non-constructive reasoning as non-monotonic learning
- Intuitionistic fixed point logic
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Extracting Herbrand disjunctions by functional interpretation
- Nondeterministic extensions of untyped \(\lambda\)-calculus
- A universal algorithm for Krull's theorem
- Probabilistic operational semantics for the lambda calculus
- Effective interactive proofs for higher-order imperative programs
- Extracting Imperative Programs from Proofs: In-place Quicksort
- Denotational cost semantics for functional languages with inductive types
- Probabilistic -calculus and Quantitative Program Analysis
- Well Quasi-orders and the Functional Interpretation
- Parameterised notions of computation
- Verification of non-functional programs using interpretations in type theory
- Gödel's functional interpretation and the concept of learning
- A functional interpretation with state
- A Graph Model for Imperative Computation
- Logic Programming
- A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
- An axiomatic basis for computer programming
- Adapting Proofs-as-Programs
- A constructive interpretation of Ramsey's theorem via the product of selection functions
- Abstract Predicates and Mutable ADTs in Hoare Type Theory
- Logical Reasoning for Higher-Order Functions with Local State
This page was built for publication: Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
