Abstract
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.
| Language | English |
|---|---|
| Pages | 1038-1078 |
| Number of pages | 41 |
| Journal | Annals of Pure and Applied Logic |
| Volume | 164 |
| Issue number | 11 |
| Early online date | 18 Jun 2013 |
| DOIs | |
| Status | Published - Nov 2013 |
Fingerprint
Cite this
Imperative programs as proofs via game semantics. / Churchill, Martin; Laird, James; McCusker, Guy.
In: Annals of Pure and Applied Logic, Vol. 164, No. 11, 11.2013, p. 1038-1078.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Imperative programs as proofs via game semantics
AU - Churchill, Martin
AU - Laird, James
AU - McCusker, Guy
N1 - Special issue on Seventh Workshop on Games for Logic and Programming Languages (GaLoP VII)
PY - 2013/11
Y1 - 2013/11
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84880699170&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1016/j.apal.2013.05.005
U2 - 10.1016/j.apal.2013.05.005
DO - 10.1016/j.apal.2013.05.005
M3 - Article
VL - 164
SP - 1038
EP - 1078
JO - Annals of Pure and Applied Logic
T2 - Annals of Pure and Applied Logic
JF - Annals of Pure and Applied Logic
SN - 0168-0072
IS - 11
ER -