A logic of sequentiality

Martin Churchill, James Laird

Research output: Chapter in Book/Report/Conference proceedingChapter

  • 5 Citations

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.
LanguageEnglish
Title of host publicationComputer Science Logic (Lecture Notes in Computer Science)
EditorsA Dawar, H Veith
PublisherSpringer
Pages215-229
Number of pages15
Volume6247/2
DOIs
StatusPublished - 24 Aug 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag

Fingerprint

Logic
Categorical
Game Semantics
Cut-elimination
Completeness
Programming
Model
Game
Higher Order
Strategy
Semantics
History

Keywords

  • full completeness
  • sequentiality
  • Game semantics

Cite this

Churchill, M., & Laird, J. (2010). A logic of sequentiality. In A. Dawar, & H. Veith (Eds.), Computer Science Logic (Lecture Notes in Computer Science) (Vol. 6247/2, pp. 215-229). (Lecture Notes in Computer Science). Springer. DOI: 10.1007/978-3-642-15205-4_19

A logic of sequentiality. / Churchill, Martin; Laird, James.

Computer Science Logic (Lecture Notes in Computer Science). ed. / A Dawar; H Veith. Vol. 6247/2 Springer, 2010. p. 215-229 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingChapter

Churchill, M & Laird, J 2010, A logic of sequentiality. in A Dawar & H Veith (eds), Computer Science Logic (Lecture Notes in Computer Science). vol. 6247/2, Lecture Notes in Computer Science, Springer, pp. 215-229. DOI: 10.1007/978-3-642-15205-4_19
Churchill M, Laird J. A logic of sequentiality. In Dawar A, Veith H, editors, Computer Science Logic (Lecture Notes in Computer Science). Vol. 6247/2. Springer. 2010. p. 215-229. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-15205-4_19
Churchill, Martin ; Laird, James. / A logic of sequentiality. Computer Science Logic (Lecture Notes in Computer Science). editor / A Dawar ; H Veith. Vol. 6247/2 Springer, 2010. pp. 215-229 (Lecture Notes in Computer Science).
@inbook{cedb3dd2ee864880a68d304a4188044b,
title = "A logic of sequentiality",
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.",
keywords = "full completeness, sequentiality, Game semantics",
author = "Martin Churchill and James Laird",
note = "Proceedings of the 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010",
year = "2010",
month = "8",
day = "24",
doi = "10.1007/978-3-642-15205-4_19",
language = "English",
volume = "6247/2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "215--229",
editor = "A Dawar and H Veith",
booktitle = "Computer Science Logic (Lecture Notes in Computer Science)",

}

TY - CHAP

T1 - A logic of sequentiality

AU - Churchill,Martin

AU - Laird,James

N1 - Proceedings of the 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010

PY - 2010/8/24

Y1 - 2010/8/24

N2 - 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.

AB - 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.

KW - full completeness

KW - sequentiality

KW - Game semantics

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

U2 - 10.1007/978-3-642-15205-4_19

DO - 10.1007/978-3-642-15205-4_19

M3 - Chapter

VL - 6247/2

T3 - Lecture Notes in Computer Science

SP - 215

EP - 229

BT - Computer Science Logic (Lecture Notes in Computer Science)

PB - Springer

ER -