Projects per year
Abstract
Game semantics extends the CurryHoward 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. We can embed intuitionistic firstorder linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a final co algebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.
Original language  English 

Title of host publication  26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011 
Publisher  IEEE 
Pages  6574 
Number of pages  10 
ISBN (Electronic)  9780769544120 
ISBN (Print)  9781457704512 
DOIs  
Publication status  Published  2011 
Event  26th Annual IEEE Symposium on Logic in Computer Science  Toronto, ON, Canada Duration: 21 Jun 2011 → 24 Jun 2011 
Publication series
Name  Annual Symposium on Logic in Computer Science 

Publisher  IEEE 
ISSN (Print)  10436871 
Conference
Conference  26th Annual IEEE Symposium on Logic in Computer Science 

Abbreviated title  LICS 2011 
Country/Territory  Canada 
City  Toronto, ON 
Period  21/06/11 → 24/06/11 
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