Projects per year
Abstract
Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Lairdʼs sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language.
The proof system has a tight connection with a simple game model, where games are forests of plays. Formulas are modelled as games, and proofs as history-sensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic (cut-free) proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics.
The proof system has a tight connection with a simple game model, where games are forests of plays. Formulas are modelled as games, and proofs as history-sensitive winning strategies. We provide a strong full completeness result with respect to this model: each finitary strategy is the denotation of a unique analytic (cut-free) proof. Infinite strategies correspond to analytic proofs that are infinitely deep. Thus, we can normalise proofs, via the semantics.
Original language | English |
---|---|
Pages (from-to) | 1038-1078 |
Number of pages | 41 |
Journal | Annals of Pure and Applied Logic |
Volume | 164 |
Issue number | 11 |
Early online date | 18 Jun 2013 |
DOIs | |
Publication status | Published - Nov 2013 |
Fingerprint
Dive into the research topics of 'Imperative programs as proofs via game semantics'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Semantic Structures for Higher-Order Information Flow
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council