Categorifying Intersection Types

Add to your list(s) Download to your calendar using vCal

• Federico Olimpieri (University of Leeds)
• Friday 29 October 2021, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Gianluca Curzi.

We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

=== ZOOM DETAILS ===

Topic: Theory Seminars Zoom Meeting Time: Oct 29, 2021 12:30 PM London

Join Zoom Meeting https://bham-ac-uk.zoom.us/j/83557617872?pwd=N2h5c2xhU1V6aHU5RnhZREtPTzk1UT09

Meeting ID: 835 5761 7872 Passcode: 846575 One tap mobile +443300885830,,83557617872# United Kingdom +441314601196,,83557617872# United Kingdom

Dial by your location +44 330 088 5830 United Kingdom +44 131 460 1196 United Kingdom +44 203 481 5237 United Kingdom +44 203 481 5240 United Kingdom +44 203 901 7895 United Kingdom +44 208 080 6591 United Kingdom +44 208 080 6592 United Kingdom Meeting ID: 835 5761 7872 Find your local number: https://bham-ac-uk.zoom.us/u/keExHEJE2C

Join by SIP 83557617872@zoomcrc.com

Join by H.323 162.255.37.11 (US West) 162.255.36.11 (US East) 115.114.131.7 (India Mumbai) 115.114.115.7 (India Hyderabad) 213.19.144.110 (Amsterdam Netherlands) 213.244.140.110 (Germany) 103.122.166.55 (Australia Sydney) 103.122.167.55 (Australia Melbourne) 149.137.40.110 (Singapore) 64.211.144.160 (Brazil) 149.137.68.253 (Mexico) 69.174.57.160 (Canada Toronto) 65.39.152.160 (Canada Vancouver) 207.226.132.110 (Japan Tokyo) 149.137.24.110 (Japan Osaka) Meeting ID: 835 5761 7872 Passcode: 846575

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.