### Abstract

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

Publication status | Published - 24 Aug 2010 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

### Fingerprint

### Keywords

- full completeness
- sequentiality
- Game semantics

### Cite this

*Computer Science Logic (Lecture Notes in Computer Science)*(Vol. 6247/2, pp. 215-229). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-642-15205-4_19

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

Research output: Chapter in Book/Report/Conference proceeding › Chapter

*Computer Science Logic (Lecture Notes in Computer Science).*vol. 6247/2, Lecture Notes in Computer Science, Springer, pp. 215-229. https://doi.org/10.1007/978-3-642-15205-4_19

}

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)

A2 - Dawar, A

A2 - Veith, H

PB - Springer

ER -