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)

115 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

Bibliographical note

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

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

Bibliographical note

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

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Projects

Semantic Structures for Higher-Order Information Flow

Cite this