Imperative programs as proofs via game semantics
From MaRDI portal
Publication:388203
DOI10.1016/j.apal.2013.05.005zbMath1358.68179arXiv1307.2004OpenAlexW4205094339MaRDI QIDQ388203
Guy McCusker, Martin Churchill, Jim Laird
Publication date: 19 December 2013
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1307.2004
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical semantics of formal languages (18C50) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items
From global to local state, coalgebraically and compositionally, Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language, From Qualitative to Quantitative Semantics, Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Resource modalities in tensor logic
- A calculus of coroutines
- A game semantics for linear logic
- Introduction to computability logic
- Focussing and proof construction
- On full abstraction for PCF: I, II and III
- Full abstraction for PCF
- Locally Boolean domains
- Locus Solum: From the rules of logic to the logic of rules
- Some Programming Languages Suggested by Game Models (Extended Abstract)
- A Categorical Semantics of Higher Order Store
- The Lambda Lambda-Bar calculus
- Game Semantics in String Diagrams
- Game semantics for first-order logic
- Classical isomorphisms of types
- Least and Greatest Fixpoints in Game Semantics
- An Explicit Formula for the Free Exponential Modality of Linear Logic
- Games and full completeness for multiplicative linear logic
- A semantics of evidence for classical arithmetic
