Projects per year
Abstract
Game semantics extends the Curry–Howard isomorphism to a threeway 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 firstorder quantification. Use of Lairdʼs sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed firstorder 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 historysensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic (cutfree) proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics.
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 historysensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic (cutfree) proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics.
Original language  English 

Pages (fromto)  10381078 
Number of pages  41 
Journal  Annals of Pure and Applied Logic 
Volume  164 
Issue number  11 
Early online date  18 Jun 2013 
DOIs  
Publication status  Published  Nov 2013 
Bibliographical note
Special issue on Seventh Workshop on Games for Logic and Programming Languages (GaLoP VII)Fingerprint
Dive into the research topics of 'Imperative programs as proofs via game semantics'. Together they form a unique fingerprint.Projects
 1 Finished

Semantic Structures for HigherOrder Information Flow
Laird, J. (PI)
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council