Imperative programs as proofs via game semantics

Martin Churchill, James Laird, Guy McCusker

Research output: Contribution to journalArticle

  • 1 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. 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.
LanguageEnglish
Pages1038-1078
Number of pages41
JournalAnnals of Pure and Applied Logic
Volume164
Issue number11
Early online date18 Jun 2013
DOIs
StatusPublished - Nov 2013

Fingerprint

Game Semantics
Linear Logic
Intuitionistic Logic
Game
First-order
Simple Game
Normalize
Lambda Calculus
Proof System
Quantification
Programming Languages
Strategy
Completeness
Isomorphism
Correspondence
Denote
Operator
Model

Cite this

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

In: Annals of Pure and Applied Logic, Vol. 164, No. 11, 11.2013, p. 1038-1078.

Research output: Contribution to journalArticle

@article{ad7ab3e826ea4e4895932f3f67ffba53,
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. 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.",
author = "Martin Churchill and James Laird and Guy McCusker",
note = "Special issue on Seventh Workshop on Games for Logic and Programming Languages (GaLoP VII)",
year = "2013",
month = "11",
doi = "10.1016/j.apal.2013.05.005",
language = "English",
volume = "164",
pages = "1038--1078",
journal = "Annals of Pure and Applied Logic",
issn = "0168-0072",
publisher = "Elsevier",
number = "11",

}

TY - JOUR

T1 - Imperative programs as proofs via game semantics

AU - Churchill, Martin

AU - Laird, James

AU - McCusker, Guy

N1 - Special issue on Seventh Workshop on Games for Logic and Programming Languages (GaLoP VII)

PY - 2013/11

Y1 - 2013/11

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

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

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

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

U2 - 10.1016/j.apal.2013.05.005

DO - 10.1016/j.apal.2013.05.005

M3 - Article

VL - 164

SP - 1038

EP - 1078

JO - Annals of Pure and Applied Logic

T2 - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

SN - 0168-0072

IS - 11

ER -