Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are 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 λ-calculus? »
JournalJ. Log. Comput.
Volume24
Number3
Page(s)557-589
Year2014
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 → !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 → !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?},
  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},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are 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)

Valid HTML 4.01!