Imperative Programs as Proofs via Game Semantics

Martin Churchill

Research output: ThesisDoctoral Thesis

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 thesis 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 a novel 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 expressive imperative total programming language. We can use the first-order structure to express properties on the imperative programs.

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

The proof system makes novel use of the fact that the sequoid operator allows the exponential modality of linear logic to be expressed as a final coalgebra.

LanguageEnglish
QualificationPh.D.
Awarding Institution
  • University of Bath
Supervisors/Advisors
  • McCusker, Guy, Supervisor
Award date1 Oct 2011
StatusUnpublished - 15 Feb 2012

Fingerprint

Semantics
Computer programming languages

Cite this

Imperative Programs as Proofs via Game Semantics. / Churchill, Martin.

2012. 251 p.

Research output: ThesisDoctoral Thesis

Churchill, M 2012, 'Imperative Programs as Proofs via Game Semantics', Ph.D., University of Bath.
Churchill, Martin. / Imperative Programs as Proofs via Game Semantics. 2012. 251 p.
@phdthesis{3612d1e18ddb4bd9ba3068e29bb885f2,
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 thesis 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 a novel 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 expressive imperative total programming language. We can use the first-order structure to express properties on the imperative programs. 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 and faithful 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. The proof system makes novel use of the fact that the sequoid operator allows the exponential modality of linear logic to be expressed as a final coalgebra.",
author = "Martin Churchill",
year = "2012",
month = "2",
day = "15",
language = "English",
school = "University of Bath",

}

TY - THES

T1 - Imperative Programs as Proofs via Game Semantics

AU - Churchill,Martin

PY - 2012/2/15

Y1 - 2012/2/15

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 thesis 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 a novel 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 expressive imperative total programming language. We can use the first-order structure to express properties on the imperative programs. 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 and faithful 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. The proof system makes novel use of the fact that the sequoid operator allows the exponential modality of linear logic to be expressed as a final coalgebra.

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 thesis 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 a novel 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 expressive imperative total programming language. We can use the first-order structure to express properties on the imperative programs. 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 and faithful 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. The proof system makes novel use of the fact that the sequoid operator allows the exponential modality of linear logic to be expressed as a final coalgebra.

M3 - Doctoral Thesis

ER -