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.

This is joint work with Federico Olimpieri, accepted at CSL 2021.

Per partecipare al Seminario cliccare sul seguente Link: https://teams.microsoft.com/dl/launcher/launcher.html?url=%2F_%23%2Fl%2Fmeetup-join%2F19%3A388bb369590943489346c5edc8bb7b83%40thread.tacv2%2F1612857243081%3Fcontext%3D%257B%2522Tid%2522%3A%2522ffb4df68-f464-458c-a546-00fb3af66f6a%2522%2C%2522Oid%2522%3A%2522a024ec6b-d39c-4c4e-b689-468d9c5b0ca8%2522%257D%26anon%3Dtrue&type=meetup-join&deeplinkId=2be82deb-6048-4772-9330-031a20d28634&directDl=true&msLaunch=true&enableMobilePage=true&suppressPrompt=true
org: PEDICINI Marco