Categorifying Non-Idempotent Intersection Types

Giulio Guerrieri; Federico Olimpieri

doi:10.4230/LIPIcs.CSL.2021.25

Categorifying Non-Idempotent Intersection Types

Giulio Guerrieri, Federico Olimpieri

Department of Computer Science

Aix-Marseille University

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

5 Citations (SciVal)

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.

Original language	English
Title of host publication	29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Editors	Christel Baier, Jean Goubault-Larrecq
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	25:1-25:24
Number of pages	24
ISBN (Electronic)	9783959771757
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2021.25
Publication status	Published - 15 Jan 2021
Event	29th EACSL Annual Conference on Computer Science Logic (CSL 2021) - Lubijana, Slovenia Duration: 25 Jan 2021 → 28 Jan 2021

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Volume	183
ISSN (Print)	1868-8969

Conference

Conference	29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Country/Territory	Slovenia
City	Lubijana
Period	25/01/21 → 28/01/21

Bibliographical note

Funding Information:
Funding This work is partially supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing.

Publisher Copyright:
© Giulio Guerrieri and Federico Olimpieri.

Keywords

Bang calculus
Bicategory
Categorification
Combinatorial species
Distributors
Linear logic
Non-idempotent intersection types
Relational semantics
Symmetric sequences

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.CSL.2021.25Licence: CC BY

Cite this

Guerrieri, G., & Olimpieri, F. (2021). Categorifying Non-Idempotent Intersection Types. In C. Baier, & J. Goubault-Larrecq (Eds.), 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) (pp. 25:1-25:24). Article 25 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 183). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2021.25

Categorifying Non-Idempotent Intersection Types. / Guerrieri, Giulio; Olimpieri, Federico.
29th EACSL Annual Conference on Computer Science Logic (CSL 2021). ed. / Christel Baier; Jean Goubault-Larrecq. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021. p. 25:1-25:24 25 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 183).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Guerrieri, G & Olimpieri, F 2021, Categorifying Non-Idempotent Intersection Types. in C Baier & J Goubault-Larrecq (eds), 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)., 25, Leibniz International Proceedings in Informatics (LIPIcs), vol. 183, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 25:1-25:24, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Lubijana, Slovenia, 25/01/21. https://doi.org/10.4230/LIPIcs.CSL.2021.25

Guerrieri G, Olimpieri F. Categorifying Non-Idempotent Intersection Types. In Baier C, Goubault-Larrecq J, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2021. p. 25:1-25:24. 25. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.CSL.2021.25

@inproceedings{facd103fc10348af954a1ef6821349d7,

title = "Categorifying Non-Idempotent Intersection Types",

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{\textquoteright}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. ",

keywords = "Bang calculus, Bicategory, Categorification, Combinatorial species, Distributors, Linear logic, Non-idempotent intersection types, Relational semantics, Symmetric sequences",

author = "Giulio Guerrieri and Federico Olimpieri",

note = "Funding Information: Funding This work is partially supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing. Publisher Copyright: {\textcopyright} Giulio Guerrieri and Federico Olimpieri.; 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) ; Conference date: 25-01-2021 Through 28-01-2021",

year = "2021",

month = jan,

day = "15",

doi = "10.4230/LIPIcs.CSL.2021.25",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "25:1--25:24",

editor = "Christel Baier and Jean Goubault-Larrecq",

booktitle = "29th EACSL Annual Conference on Computer Science Logic (CSL 2021)",

address = "Germany",

}

TY - GEN

T1 - Categorifying Non-Idempotent Intersection Types

AU - Guerrieri, Giulio

AU - Olimpieri, Federico

N1 - Funding Information: Funding This work is partially supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing. Publisher Copyright: © Giulio Guerrieri and Federico Olimpieri.

PY - 2021/1/15

Y1 - 2021/1/15

N2 - 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.

AB - 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.

KW - Bang calculus

KW - Bicategory

KW - Categorification

KW - Combinatorial species

KW - Distributors

KW - Linear logic

KW - Non-idempotent intersection types

KW - Relational semantics

KW - Symmetric sequences

UR - http://www.scopus.com/inward/record.url?scp=85100897957&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2021.25

DO - 10.4230/LIPIcs.CSL.2021.25

M3 - Chapter in a published conference proceeding

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 25:1-25:24

BT - 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

A2 - Baier, Christel

A2 - Goubault-Larrecq, Jean

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Y2 - 25 January 2021 through 28 January 2021

ER -

Categorifying Non-Idempotent Intersection Types

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

Categorifying Non-Idempotent Intersection Types

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this