Categorical Models for a Semantically Linear Lambda-calculus

Marco Gaboardi
Mauro Piccolo

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.

In Mário Florido and Ian Mackie: Proceedings First International Workshop on Linearity (LINEARITY 2009), Coimbra, Portugal, 12th September 2009, Electronic Proceedings in Theoretical Computer Science 22, pp. 1–13.
Published: 30th March 2010.

ArXived at: https://dx.doi.org/10.4204/EPTCS.22.1 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org