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 language | English |
---|---|
Journal | Journal of Logic and Computation |
Early online date | 12 Jun 2012 |
DOIs | |
Publication status | Published - 2012 |
Keywords
- linearity
- PCF
- categorical models
- completeness