A logic of sequentiality

Martin Churchill, James Laird

Research output: Chapter in Book/Report/Conference proceedingChapter

5 Citations (Scopus)
33 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 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
Publication statusPublished - 24 Aug 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag

Keywords

  • full completeness
  • sequentiality
  • Game semantics

Fingerprint Dive into the research topics of 'A logic of sequentiality'. Together they form a unique fingerprint.

Cite this