Projects per year
Abstract
Game semantics has been used to interpret both proofs and functional programs: an important further development on the programming side has been to model higherorder programs with state by allowing strategies with ``historysensitive'' behaviour. In this paper, we develop a detailed analysis of the structure of these strategies from a logical perspective by showing that they correspond to proofs in a new kind of affine logic.
We describe the semantics of our logic formally by giving a notion of categorical model and an instance based on a simple category of games. Using further categorical properties of this model, we prove a full completeness result: each total strategy is the semantics of a unique cutfree \emph{core} proof in the system. We then use this result to derive an explicit cutelimination procedure.
We describe the semantics of our logic formally by giving a notion of categorical model and an instance based on a simple category of games. Using further categorical properties of this model, we prove a full completeness result: each total strategy is the semantics of a unique cutfree \emph{core} proof in the system. We then use this result to derive an explicit cutelimination procedure.
Original language  English 

Title of host publication  Computer Science Logic (Lecture Notes in Computer Science) 
Editors  A Dawar, H Veith 
Publisher  Springer 
Pages  215229 
Number of pages  15 
Volume  6247/2 
DOIs  
Publication status  Published  24 Aug 2010 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer Verlag 
Keywords
 full completeness
 sequentiality
 Game semantics
Fingerprint
Dive into the research topics of 'A logic of sequentiality'. Together they form a unique fingerprint.Projects
 1 Finished

Semantic Structures for HigherOrder Information Flow
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council