Imperative programs as proofs via game semantics

Martin Churchill; James Laird; Guy McCusker

doi:10.1109/LICS.2011.19

Imperative programs as proofs via game semantics

Martin Churchill, James Laird, Guy McCusker

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

4 Citations (SciVal)

254 Downloads (Pure)

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. 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 language	English
Title of host publication	26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011
Publisher	IEEE
Pages	65-74
Number of pages	10
ISBN (Electronic)	9780769544120
ISBN (Print)	9781457704512
DOIs	https://doi.org/10.1109/LICS.2011.19
Publication status	Published - 2011
Event	26th Annual IEEE Symposium on Logic in Computer Science - Toronto, ON, Canada Duration: 21 Jun 2011 → 24 Jun 2011

Publication series

Name	Annual Symposium on Logic in Computer Science
Publisher	IEEE
ISSN (Print)	1043-6871

Conference

Conference	26th Annual IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2011
Country/Territory	Canada
City	Toronto, ON
Period	21/06/11 → 24/06/11

Access to Document

10.1109/LICS.2011.19

CLM11.pdf
© 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

Cite this

@inproceedings{b8cfb09cb581443da14e5773e8481533,

title = "Imperative programs as proofs via game semantics",

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. 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.",

author = "Martin Churchill and James Laird and Guy McCusker",

year = "2011",

doi = "10.1109/LICS.2011.19",

language = "English",

isbn = "9781457704512",

series = "Annual Symposium on Logic in Computer Science",

publisher = "IEEE",

pages = "65--74",

booktitle = "26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011",

address = "USA United States",

note = "26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011 ; Conference date: 21-06-2011 Through 24-06-2011",

}

TY - GEN

T1 - Imperative programs as proofs via game semantics

AU - Churchill, Martin

AU - Laird, James

AU - McCusker, Guy

PY - 2011

Y1 - 2011

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

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

UR - http://www.scopus.com/inward/record.url?scp=80052172689&partnerID=8YFLogxK

UR - http://dx.doi.org/10.1109/LICS.2011.19

U2 - 10.1109/LICS.2011.19

DO - 10.1109/LICS.2011.19

M3 - Chapter in a published conference proceeding

SN - 9781457704512

T3 - Annual Symposium on Logic in Computer Science

SP - 65

EP - 74

BT - 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011

PB - IEEE

T2 - 26th Annual IEEE Symposium on Logic in Computer Science

Y2 - 21 June 2011 through 24 June 2011

ER -

Imperative programs as proofs via game semantics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Semantic Structures for Higher-Order Information Flow

Cite this

Imperative programs as proofs via game semantics

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Projects

Semantic Structures for Higher-Order Information Flow

Cite this