Synchronous Games, Simulations and lambda-calculus

TL;DR

This paper refines a game-based model of linear logic to include computational content, interpreting lambda-calculus and differential lambda-calculus constructively within a synchronous framework.

Contribution

It introduces a constructive interpretation of simulation relations in linear logic, extending to lambda-calculus and differential lambda-calculus models.

Findings

Constructive models for typed lambda-calculus

Denotational models for differential lambda-calculus

Extension of synchronous game semantics to computational content

Abstract

We refine a model for linear logic based on two well-known ingredients: games and simulations. We have already shown that usual simulation relations form a sound notion of morphism between games; and that we can interpret all linear logic in this way. One particularly interesting point is that we interpret multiplicative connectives by synchronous operations on games. We refine this work by giving computational contents to our simulation relations. To achieve that, we need to restrict to intuitionistic linear logic. This allows to work in a constructive setting, thus keeping a computational content to the proofs. We then extend it by showing how to interpret some of the additional structure of the exponentials. To be more precise, we first give a denotational model for the typed lambda-calculus; and then give a denotational model for the differential lambda-calculus of Ehrhard and Regnier. Both this models are proved correct constructively.