Imperative programs as proofs via game semantics

DOI10.1016/J.APAL.2013.05.005MaRDI QIDQ388203zbMATH OpenOpenAlexFDO

Authors Martin Churchill, Guy McCusker, 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

full completenessgame semanticshistory-sensitive strategiessequentiality

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical semantics of formal languages (18C50) Semantics in the theory of computing (68Q55)

Abstract: Game semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Laird's sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language. The proof system has a tight connection with a simple game model, where games are forests of plays. Formulas are modelled as games, and proofs as history-sensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic (cut-free) proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics.

Recommendations

• A logic of sequentiality
• A parallel game semantics for linear logic
• Games and full completeness for multiplicative linear logic
• Constructive game logic
• scientific article; zbMATH DE number 1241700

Cites work

• A calculus of coroutines
• A categorical semantics of higher order store
• A game semantics for linear logic
• A note on actions of a monoidal category
• A semantics of evidence for classical arithmetic
• An Explicit Formula for the Free Exponential Modality of Linear Logic
• Classical isomorphisms of types
• Focussing and proof construction
• Full abstraction for PCF
• Game semantics for first-order logic
• Game Semantics in String Diagrams
• Games and full completeness for multiplicative linear logic
• scientific article; zbMATH DE number 1231510 (Why is no real title available?)
• scientific article; zbMATH DE number 1241700 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• Introduction to computability logic
• Least and Greatest Fixpoints in Game Semantics
• Locally Boolean domains
• Locus solum: From the rules of logic to the logic of rules.
• On full abstraction for PCF: I, II and III
• Resource modalities in tensor logic
• Some programming languages suggested by game models (extended abstract)
• The lambda -bar calculus, a dual calculus for unconstrained strategies

Cited in

(8)

• Theories for mechanical proofs of imperative programs
• From global to local state, coalgebraically and compositionally
• From qualitative to quantitative semantics. By change of base
• A logic of sequentiality
• Study of behaviours via visitable paths
• Constructive game logic
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• An axiomatic account of a fully abstract game semantics for general references

This page was built for publication: Imperative programs as proofs via game semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q388203)