A logic of sequentiality

Reference:

Churchill, M. and Laird, J., 2010. A logic of sequentiality. In: Dawar , A. and Veith, H., eds. Computer Science Logic (Lecture Notes in Computer Science). Springer Verlag, pp. 215-229.

Official URL:

http://www.springerlink.com/content/r62nw77228k232q2/

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 higher-order programs with state by allowing strategies with ``history-sensitive'' 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 cut-free \emph{core} proof in the system. We then use this result to derive an explicit cut-elimination procedure.

Details

Item Type	Book Sections
Creators	Churchill, M.and Laird, J.
Editors	Dawar , A.and Veith, H.
DOI	10.1007/978-3-642-15205-4_19
Uncontrolled Keywords	Game semantics, sequentiality, full completeness
Departments	Faculty of Science > Computer Science
Publisher Statement	Proceedings of CSL 2010, Springer Verlag, Editors A. Dawar and H. Veith. The original publication is available at: http://www.springerlink.com/content/r62nw77228k232q2
Funders	Engineering and Physical Sciences Research Council (EPSRC)
Refereed	Yes
Status	Published
ID Code	20970
Additional Information	Proceedings of the 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010

Find a copy

Export

Actions (login required)

View Item

Document Downloads

More statistics for this item...

Research