Projects per year
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. We can embed intuitionistic first-order linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a final co algebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.
|Title of host publication||26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011|
|Number of pages||10|
|Publication status||Published - 2011|
|Event||26th Annual IEEE Symposium on Logic in Computer Science - Toronto, ON, Canada|
Duration: 21 Jun 2011 → 24 Jun 2011
|Name||Annual Symposium on Logic in Computer Science|
|Conference||26th Annual IEEE Symposium on Logic in Computer Science|
|Abbreviated title||LICS 2011|
|Period||21/06/11 → 24/06/11|
FingerprintDive into the research topics of 'Imperative programs as proofs via game semantics'. Together they form a unique fingerprint.
- 1 Finished
20/06/10 → 19/06/12
Project: Research council