Coherence Spaces and Uniform Continuity

Abstract

In this paper, we consider a model of classical linear logic based on coherence spaces endowed with a notion of totality. If we restrict ourselves to total objects, each coherence space can be regarded as a uniform space and each linear map as a uniformly continuous function. The linear exponential comonad then assigns to each uniform space X the finest uniform space !X compatible with X. By a standard realizability construction, it is possible to consider a theory of representations in our model. Each (separable, metrizable) uniform space, such as the real line, can then be represented by (a partial surjecive map from) a coherence space with totality. The following holds under certain mild conditions: a function between uniform spaces X and Y is uniformly continuous if and only if it is realized by a total linear map between the coherence spaces representing X and Y.