# Imperative programs as proofs via game semantics

### Reference:

Churchill, M., Laird, J. and McCusker, G., 2013. Imperative programs as proofs via game semantics. Annals of Pure and Applied Logic, 164 (11), pp. 1038-1078.

### Related documents:

 Preview
PDF (Author's accepted version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

### Official URL:

http://dx.doi.org/10.1016/j.apal.2013.05.005

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

### Details

Item Type Articles
CreatorsChurchill, M., Laird, J. and McCusker, G.
DOI10.1016/j.apal.2013.05.005
Related URLs
URLURL Type
http://www.scopus.com/inward/record.url?scp=84880699170&partnerID=8YFLogxKUNSPECIFIED
DepartmentsFaculty of Science > Computer Science
Publisher Statementjournal2.pdf: NOTICE: this is the author’s version of a work that was accepted for publication in Annals of Pure and Applied Logic. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Annals of Pure and Applied Logic, 2013, DOI 10.1016/j.apal.2013.05.005
RefereedYes
StatusPublished
ID Code35817
Additional InformationSpecial issue on Seventh Workshop on Games for Logic and Programming Languages (GaLoP VII)

### Actions (login required)

 View Item