Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

 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) 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 $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.

 BibTeX code

@article{gaboardi14jlc,
number = {3},
volume = {24},
author = {Marco Gaboardi and Mauro Piccolo},
title = {What is a model for a semantically linear $\lambda$-calculus?},
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},
}

 Formal Methods in Computing(Most of the papers antecedent to 1995are not included in the list) FRAMES  NO FRAME

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)