Categorifying Non-Idempotent Intersection Types

Giulio Guerrieri, Federico Olimpieri

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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
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)


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

Cite this