DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2024.43

Coherence by Normalization for Linear Multicategorical Structures

Authors: Federico Olimpieri

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract

We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane’s coherence theorems for (symmetric) monoidal categories.

Cite as

Federico Olimpieri. Coherence by Normalization for Linear Multicategorical Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 43:1-43:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{olimpieri:LIPIcs.CSL.2024.43,
  author =	{Olimpieri, Federico},
  title =	{{Coherence by Normalization for Linear Multicategorical Structures}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{43:1--43:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.43},
  URN =		{urn:nbn:de:0030-drops-196865},
  doi =		{10.4230/LIPIcs.CSL.2024.43},
  annote =	{Keywords: Coherence, Linear Multicategories, Resource Calculi, Normalization}
}

Document

DOI: 10.4230/LIPIcs.CSL.2021.25

Categorifying Non-Idempotent Intersection Types

Authors: Giulio Guerrieri and Federico Olimpieri

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of the bang calculus, an untyped version of Levy’s call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0.

Cite as

Giulio Guerrieri and Federico Olimpieri. Categorifying Non-Idempotent Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{guerrieri_et_al:LIPIcs.CSL.2021.25,
  author =	{Guerrieri, Giulio and Olimpieri, Federico},
  title =	{{Categorifying Non-Idempotent Intersection Types}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{25:1--25:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.25},
  URN =		{urn:nbn:de:0030-drops-134592},
  doi =		{10.4230/LIPIcs.CSL.2021.25},
  annote =	{Keywords: Linear logic, bang calculus, non-idempotent intersection types, distributors, relational semantics, combinatorial species, symmetric sequences, bicategory, categorification}
}

Search Results

Documents authored by Olimpieri, Federico

Coherence by Normalization for Linear Multicategorical Structures

Abstract

Cite as

Categorifying Non-Idempotent Intersection Types

Abstract

Cite as

Thanks for your feedback!

Could not send message