This is the first of a series of papers on coherence completions of categories. Here we show that there is a close connection between Girard's coherence spaces and free bicomplete categories. We introduce a new construction for creating models of linear logic, the coherence completion of a category. By presenting coherence completions as categories enriched over the category of pointed sets and the category of coherence spaces, the free structures on coherence completions are obtained in a very natural way. We show that if C is monoidal closed or ★-autonomous then so is its coherence completion. We also prove that if C is a model of linear logic then so is its coherence completion. A key idea of the paper which is introduced into linear logic is the notion of softness. We hope that this idea could be of use in solving the full completeness for larger fragments of linear logic.

An abstract definition of bisimulation is presented. It allows a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronization trees, transition systems with independence (an abstraction from Petri nets), and labeled event structures are considered. On transition systems, the abstract definition readily specialises to Milner's (1989) strong bisimulation. On event structures, it explains and leads to a revision of the history-preserving bisimulation of Rabinovitch and Traktenbrot (1988), and Goltz and van Glabeek (1989). A tie-up with open maps in a (pre)topos brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labeled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has refinement operators, though further work is required to justify their appropriateness and understand their relation to previous attempts.>

Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie algébrique sous la forme élaborée par Grothendieck. (2) La logique formelle. Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes: (1) Mathématique intuitionniste. (2) Forcing de Cohen et Robinson. (3) Logique algébrique. (4) Géométrie algébrique. (5) Géométrie différentielle et analytique. (6) Topologie algébrique: cohomologie, homotopie. (7) Théorie de Galois. Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3). La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8]. Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].