Categorical Models for a Semantically Linear Lambda-calculus

TL;DR

This paper introduces Sll-Category, a categorical framework that models a simple Semantically Linear lambda calculus underlying SlPCF, extending existing linear categories to encompass a broad class of sound models.

Contribution

It defines Sll-Category, a new categorical structure that soundly interprets all constructs of Sll-calculus, broadening the scope of models including Scott Domains and Coherence Spaces.

Findings

Sll-Category extends Linear Categories to model Sll-calculus.

The framework captures models in Scott Domains and Coherence Spaces.

It provides a sound categorical semantics for a linear lambda calculus.

Abstract

This paper is about a categorical approach to model a very simple Semantically Linear lambda calculus, named Sll-calculus. This is a core calculus underlying the programming language SlPCF. In particular, in this work, we introduce the notion of Sll-Category, which is able to describe a very large class of sound models of Sll-calculus. Sll-Category extends in the natural way Benton, Bierman, Hyland and de Paiva's Linear Category, in order to soundly interpret all the constructs of Sll-calculus. This category is general enough to catch interesting models in Scott Domains and Coherence Spaces.