What is a Model for a Semantically Linear Lambda-calculus?

Abstract : This paper is about a categorical approach to model a very simple Semantically Linear lambda calculus, named Sll-calculus. This is a core calculus underlying the programming language SlPCF. In particular, in this work, we introduce the notion of Sll-Category, which is able to describe a very large class of sound models of Sll-calculus. Sll-Category extends in the natural way Benton, Bierman, Hyland and de Paiva's Linear Category, in order to soundly interpret all the constructs of Sll-calculus. This category is general enough to catch interesting models in Scott Domains and Coherence Spaces.
Type de document :
Article dans une revue
Journal of Logic and Computation, Oxford University Press (OUP), 2012, 〈10.1093/logcom/exs023〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00909362
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:07:24
Dernière modification le : samedi 27 janvier 2018 - 01:31:36

Lien texte intégral

Identifiants

Collections

INRIA | PPS | USPC

Citation

Marco Gaboardi, Mauro Piccolo. What is a Model for a Semantically Linear Lambda-calculus?. Journal of Logic and Computation, Oxford University Press (OUP), 2012, 〈10.1093/logcom/exs023〉. 〈hal-00909362〉

Partager

Métriques

Consultations de la notice

159