Categorifying Non-Idempotent Intersection Types

Giulio Guerrieri, Federico Olimpieri

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

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 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
Pages25:1-25:24
Number of pages24
DOIs
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)
Volume183

Conference

Conference29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
CountrySlovenia
CityLubijana
Period25/01/2128/01/21

Cite this