Imperative programs as proofs via game semantics

Martin Churchill, James Laird, Guy McCusker

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

4 Citations (SciVal)
195 Downloads (Pure)


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.
Original languageEnglish
Title of host publication26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011
Number of pages10
ISBN (Electronic)9780769544120
ISBN (Print)9781457704512
Publication statusPublished - 2011
Event26th Annual IEEE Symposium on Logic in Computer Science - Toronto, ON, Canada
Duration: 21 Jun 201124 Jun 2011

Publication series

NameAnnual Symposium on Logic in Computer Science
ISSN (Print)1043-6871


Conference26th Annual IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2011
CityToronto, ON


Dive into the research topics of 'Imperative programs as proofs via game semantics'. Together they form a unique fingerprint.

Cite this