A logic of sequentiality

Martin Churchill; James Laird

doi:10.1007/978-3-642-15205-4_19

A logic of sequentiality

Martin Churchill, James Laird

Research output: Chapter or section in a book/report/conference proceeding › Chapter or section

6 Citations (SciVal)

74 Downloads (Pure)

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.

Original language	English
Title of host publication	Computer Science Logic (Lecture Notes in Computer Science)
Editors	A Dawar, H Veith
Publisher	Springer
Pages	215-229
Number of pages	15
Volume	6247/2
DOIs	https://doi.org/10.1007/978-3-642-15205-4_19
Publication status	Published - 24 Aug 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag

Keywords

full completeness
sequentiality
Game semantics

Access to Document

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

csl10.pdf
Proceedings of CSL 2010, Springer Verlag, Editors A. Dawar and H. Veith. The original publication is available at: http://www.springerlink.com/content/r62nw77228k232q2
Submitted manuscript, 456 KB

Cite this

@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 = aug,

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 or section

VL - 6247/2

T3 - Lecture Notes in Computer Science

SP - 215

EP - 229

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

A2 - Dawar, A

A2 - Veith, H

PB - Springer

ER -

A logic of sequentiality

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Semantic Structures for Higher-Order Information Flow

Cite this

A logic of sequentiality

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Semantic Structures for Higher-Order Information Flow

Cite this