Categorical Models for a Semantically Linear Lambda-calculus
Logic in Computer Science
2010-03-30 v1
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.
Keywords
Cite
@article{arxiv.1003.5511,
title = {Categorical Models for a Semantically Linear Lambda-calculus},
author = {Marco Gaboardi and Mauro Piccolo},
journal= {arXiv preprint arXiv:1003.5511},
year = {2010}
}