Hypercoherences: a strongly stable model of linear logic
Thomas Ehrhard · Cambridge University Press eBooks · 1993
We present a model of classical linear logic based on the notion of strong stability that was introduced in [BE], a work about sequentiality written jointly with Antonio Bucciarelli. Introduction The present article is a new version of an article already published, with the same title, in Mathematical Structures in Computer Science (1993), vol. 3, pp. 365–385. It is identical to this previous version, except for a few minor details. In the denotational semantics of purely functional languages (such as PCF [P, BCL]), types are interpreted as objects and programs as morphisms in a cartesian closed category (CCC for short). Usually, the objects of this category are at least Scott domains, and the morphisms are at least continuous functions. The goal of denotational semantics is to express, in terms of “abstract” properties of these functions, some interesting computational properties of the language. One of these abstract properties is “continuity”. It corresponds to the basic fact that any computation that terminates can use only a finite amount of data. The corresponding semantics of PCF is the continuous one, where objects are Scott domains, and morphisms continuous functions. But the continuous semantics does not capture an important property of computations in PCF, namely “determinism”. Vuillemin and Milner are at the origin of the first (equivalent) definitions of sequentiality , a semantic notion corresponding to determinism. Kahn and Plotkin ([KP]) generalized this notion of sequentiality. More precisely, they defined a category of “concrete domains” (represented by “concrete data structures”) and of sequential functions.