gaboardi14jlc (Article)

Author(s)  Marco Gaboardi and Mauro Piccolo 
Title  « What is a model for a semantically linear $\lambda $calculus? » 
Journal  J. Log. Comput. 
Volume  24 
Number  3 
Page(s)  557589 
Year  2014 
Abstract 
This article is about a categorical approach modelling a simple term calculus, named Sllambdacalculus. This is the core calculus underlying the programming language SlPCF conceived in order to program only linear functions between coherence spaces. We introduce the notion of Sllambdacategory, which is able to describe a large class of sound models of Sllambdacalculus. An Sllambdacategory extends in a natural way Benton, Bierman, Hyland and de Paivaâ€™s Linear Category by requirements useful to interpret all the programming constructs of the S Î»calculus. In particular, a key role is played by a !coalgebra $p\; :\; N\; \to \; !N$ used to interpret the numeral constants of the Sllambdacalculus. We will define two interpretations of Sllambdacalculus types and terms into objects and morphisms of Sllambdacategories: the first one is a generalization of the translation given in [23] but lacks completeness; the second one uses the !coalgebra $p\; :\; N\; \to \; !N$ and the comonadic properties of ! to recover completeness. Finally, we show that this notion is general enough to capture interesting models in the category of sets and relations, in Scott Domains and in coherence spaces. 
@article{gaboardi14jlc,
number = {3},
volume = {24},
author = {Marco Gaboardi and Mauro Piccolo},
title = {What is a model for a semantically linear $\lambda$calculus?},
abstract = {This article is about a categorical approach modelling a simple
term calculus, named Sllambdacalculus. This is the core calculus
underlying the programming language SlPCF conceived in order to
program only linear functions between coherence spaces. We
introduce the notion of Sllambdacategory, which is able to
describe a large class of sound models of Sllambdacalculus. An
Sllambdacategory extends in a natural way Benton, Bierman, Hyland
and de Paivaâ€™s Linear Category by requirements useful to
interpret all the programming constructs of the S Î»calculus. In
particular, a key role is played by a !coalgebra $p : N \to !N$
used to interpret the numeral constants of the Sllambdacalculus.
We will define two interpretations of Sllambdacalculus types and
terms into objects and morphisms of Sllambdacategories: the first
one is a generalization of the translation given in [23] but lacks
completeness; the second one uses the !coalgebra $p : N \to !N$
and the comonadic properties of ! to recover completeness.
Finally, we show that this notion is general enough to capture
interesting models in the category of sets and relations, in Scott
Domains and in coherence spaces.},
journal = {J. Log. Comput.},
year = {2014},
pages = {557589},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)