Categorifying Non-Idempotent Intersection Types

Giulio Guerrieri, Federico Olimpieri

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

4 Citations (SciVal)


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 languageEnglish
Title of host publication29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
EditorsChristel Baier, Jean Goubault-Larrecq
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages24
ISBN (Electronic)9783959771757
Publication statusPublished - 15 Jan 2021
Event29th EACSL Annual Conference on Computer Science Logic (CSL 2021) - Lubijana, Slovenia
Duration: 25 Jan 202128 Jan 2021

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
ISSN (Print)1868-8969


Conference29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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.


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

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Categorifying Non-Idempotent Intersection Types'. Together they form a unique fingerprint.

Cite this