Quantitative Domains, Groupoids and Linear Logic

We introduce the notion of a candidate for “multiple valued universal constructions” and define stable functors (which generalise functors with left adjoints) in terms of factorisation through candidates. There are many mathematical examples, including the Zariski spectrum of a ring (as shown by Diers [81]) and the Galois group of a polynomial, but we are mainly interested in Berry’s [78] minimum data property. In fact we begin with a completely nonmathematical example. The aim is to find domain models in which terms of the typed or polymorphic λ-calculus are interpreted as stable functors. We study Girard’s quantitative domains [85], in which information is represented by a collection of tokens from a universe of tokens for a particular type, and there is no restriction on the ability of different tokens to co-exist or on the number of occurrences of a particular token. This idea may be used to code parallelism (with no suppression of duplicated output) or accounted resou...

• Type: Conference
• Year: 1989
• Where: CTCS
• Authors: Paul Taylor 0002
• Keywords: CTCS 1989, Girard’s Quantitative Domains, Programming Languages, Quantitative Domains, Stable Functors