Functional Interpretations of Intuitionistic Linear Logic

TL;DR

This paper introduces three new functional interpretations of intuitionistic linear logic, simplifying previous approaches and connecting them to known interpretations of intuitionistic logic through embeddings.

Contribution

It provides novel, simplified functional interpretations of ILL that avoid the complexity of simultaneous quantifiers and relate to existing interpretations via embeddings.

Findings

Three functional interpretations of ILL are developed.

Simplification of interpretations compared to previous work.

Connections established between ILL interpretations and intuitionistic logic.

Abstract

We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic logic IL via embeddings of IL into ILL. The main difference from previous work of the second author is that in intuitionistic linear logic (as opposed to classical linear logic) the interpretations of !A are simpler and simultaneous quantifiers are no longer needed for the characterisation of the interpretations. We then compare our approach in developing these three proof interpretations with the one of de Paiva around the Dialectica category model of linear logic.