Imperative programs as proofs via game semantics

Martin Churchill, James Laird, Guy McCusker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

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.
LanguageEnglish
Title of host publication26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011
PublisherIEEE
Pages65-74
Number of pages10
ISBN (Electronic)9780769544120
ISBN (Print)9781457704512
DOIs
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
PublisherIEEE
ISSN (Print)1043-6871

Conference

Conference26th Annual IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2011
CountryCanada
CityToronto, ON
Period21/06/1124/06/11

Fingerprint

Game Semantics
Logic
Linear Logic
Intuitionistic Logic
Lambda Calculus
Coalgebra
First-order Logic
Programming Languages
Completeness
Isomorphism
Correspondence
Denote
Strategy
Theorem

Cite this

Churchill, M., Laird, J., & McCusker, G. (2011). Imperative programs as proofs via game semantics. In 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011 (pp. 65-74). (Annual Symposium on Logic in Computer Science). IEEE. https://doi.org/10.1109/LICS.2011.19

Imperative programs as proofs via game semantics. / Churchill, Martin; Laird, James; McCusker, Guy.

26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011. IEEE, 2011. p. 65-74 (Annual Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Churchill, M, Laird, J & McCusker, G 2011, Imperative programs as proofs via game semantics. in 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011. Annual Symposium on Logic in Computer Science, IEEE, pp. 65-74, 26th Annual IEEE Symposium on Logic in Computer Science, Toronto, ON, Canada, 21/06/11. https://doi.org/10.1109/LICS.2011.19
Churchill M, Laird J, McCusker G. Imperative programs as proofs via game semantics. In 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011. IEEE. 2011. p. 65-74. (Annual Symposium on Logic in Computer Science). https://doi.org/10.1109/LICS.2011.19
Churchill, Martin ; Laird, James ; McCusker, Guy. / Imperative programs as proofs via game semantics. 26th Annual IEEE Symposium on Logic in Computer Science (LICS) 2011. IEEE, 2011. pp. 65-74 (Annual Symposium on Logic in Computer Science).
@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",

}

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 - Conference contribution

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

ER -