What is a model for a semantically linear ?-calculus?

Marco Gaboardi, Mauro Piccolo

    Research output: Contribution to journalArticlepeer-review

    Abstract

    This article is about a categorical approach modelling a simple term calculus, named ?l?-calculus. This is the core calculus underlying the programming language ?lPCF conceived in order to program only linear functions between coherence spaces. We introduce the notion of ?l?-category, which is able to describe a large class of sound models of ?l?-calculus. An ?l?-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 ?l?-calculus. In particular, a key role is played by a !-coalgebra p:N?!N used to interpret the numeral constants of the ?l?-calculus. We will define two interpretations of ?l?-calculus types and terms into objects and morphisms of ?l?-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.
    Original languageEnglish
    JournalJournal of Logic and Computation
    Early online date12 Jun 2012
    DOIs
    Publication statusPublished - 2012

    Keywords

    • linearity
    • PCF
    • categorical models
    • completeness

    Fingerprint Dive into the research topics of 'What is a model for a semantically linear ?-calculus?'. Together they form a unique fingerprint.

    Cite this