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