Projects per year
Abstract
Nonidempotent intersection types can be seen as a syntactic presentation of a wellknown denotational semantics for the lambdacalculus, 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 callbypushvalue. 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 GoubaultLarrecq 
Publisher  Schloss Dagstuhl LeibnizZentrum fur Informatik GmbH, Dagstuhl Publishing 
Pages  25:125:24 
Number of pages  24 
DOIs  
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 
Conference
Conference  29th EACSL Annual Conference on Computer Science Logic (CSL 2021) 

Country  Slovenia 
City  Lubijana 
Period  25/01/21 → 28/01/21 
Projects
 1 Active

Typed LambdaCalculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 31/12/21
Project: Research council