c©Marco Gaboardi and Mauro Piccolo This work is licensed under the Creative Commons Attribution License. Categorical Models for a Semantically Linear λ-calculus∗

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