Imperative Programs as Proofs via Game Semantics

TL;DR

This paper extends game semantics to include imperative and stateful programs, providing a logical framework where proofs denote strategies, enabling normalization and embedding of linear logic into a game-theoretic setting.

Contribution

It introduces Polarized Linear Logic, a system capturing imperative behavior within game semantics, with a full completeness result linking strategies to proofs.

Findings

Finitary strategies correspond to unique cut-free proofs.

Infinite strategies relate to infinitely deep analytic proofs.

Proof normalization is achieved through semantic interpretation.

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.