@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)