Imperative Programs as Proofs via Game Semantics

Photograph of Martin Churchill

Martin Churchill

(University of Bath)

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 talk 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 coalgebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof.
(Joint work with Jim Laird and Guy McCusker)

Thursday 24th February 2011, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science