Imperative programs as proofs via game semantics

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

zbMATH Keywords

game semanticssequentialityfull completenesshistory-sensitive strategies

Mathematics Subject Classification ID

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