Generalized generalized species of structure and resource modalities

Author: Luc Pellissier

Paper Information

Title:Generalized generalized species of structure and resource modalities
Authors:Luc Pellissier
Proceedings:Linearity/TLLA Pre-proceedings
Editors: Maribel Fernandez, Valeria de Paiva, Thomas Ehrhard and Lorenzo Tortora De Falco
Keywords:Linear Logic, Intersection Type Systems, Operad, Species of Structures

ABSTRACT. We propose to return to the construction carried precedently, where we claimed that Simply-typed approximations = intersection types derivations in the precise sense that we built a categorical equivalence between specific type systems (that encompass all well-known intersection type systems used to characterize normalization) and simply-typed approximations, that we realize as approximation functors, that arise from the translation of the language into linear logic. By studying these specific functors, we claim that their main feature is that they map the exponential of linear logic into what can reasonably be called a resource modality, corresponding either to linear, affine or cartesian intersection types. So, we present the story under the slightly different, and less syntactic, slogan: Intersection type system = multiplicative linear logic + resource modality These resource modalities are linked with well-know systems. In particular, generalized species of structure can be seen as a strictification of the Kleisli category of the linear resource modality. The study of the link between these different resource modality can shed a new light on the extensional collapse, and paving the way for a study of this collapse for dynamic semantics (such as the Geometry of Interaction and ordered combinatory algebras, used to account for forcing and realizability).

Talk:Jul 08 14:00 (Session 40L)