Quillen model structures, *-autonomous categories and adherence spaces

Abstract

Linear logic has been intensively studied since its introduction almost twenty years ago. Originally introduced as a proof theory, two distinct semantic traditions have evolved around linear logic: the denotational semantics of linear logic, and the Geometry of Interaction. In this thesis we explore how abstract homotopy theory may be used to reconcile these semantic traditions. This approach is in some sense already suggested by the fact that, in denotational semantics, one is forced to take equivalence classes of proofs, and not proofs per se, as morphisms. Our approach amounts to taking a coarser equivalence relation than is needed to construct a denotational model, in order to create a category more closely resembling those which occur in Geometry of Interaction. A new class of denotational models, called adherence spaces and in some sense tailor-suited to the problem at hand, are introduced. Then it is shown how a Quillen model structure may be imposed on a category of adherence spaces in such a way that the resulting homotopy category is compact closed.