gaboardi14jlc (Article)
|
Author(s) | Marco Gaboardi and Mauro Piccolo |
Title | « What is a model for a semantically linear -calculus? » |
Journal | J. Log. Comput. |
Volume | 24 |
Number | 3 |
Page(s) | 557-589 |
Year | 2014 |
Abstract |
This article is about a categorical approach modelling a simple term calculus, named Sllambda-calculus. 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 Sllambda-category, which is able to describe a large class of sound models of Sllambda-calculus. An Sllambda-category 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 used to interpret the numeral constants of the Sllambda-calculus. We will define two interpretations of Sllambda-calculus types and terms into objects and morphisms of Sllambda-categories: the first one is a generalization of the translation given in [23] but lacks completeness; the second one uses the !-coalgebra 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 Sllambda-calculus. 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 Sllambda-category, which is able to
describe a large class of sound models of Sllambda-calculus. An
Sllambda-category 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 Sllambda-calculus.
We will define two interpretations of Sllambda-calculus types and
terms into objects and morphisms of Sllambda-categories: 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 = {557-589},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)