BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Federico Olimpieri (University of Leeds)
DTSTART:20211118T143000Z
DTEND:20211118T153000Z
DTSTAMP:20260423T021447Z
UID:itaca/12
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/itaca/12/">C
 ategorifying Intersection Types</a>\nby Federico Olimpieri (University of 
 Leeds) as part of ItaCa Fest 2021\n\n\nAbstract\nWe study a family of dist
 ributors-induced bicategorical models of lambda-calculus\, proving that th
 ey can be syntactically presented via intersection type systems. We first 
 introduce a class of 2-monads whose algebras are monoidal categories model
 ling resource management. We lift these monads to distributors and define 
 a parametric Kleisli bicategory\, giving a sufficient condition for its ca
 rtesian closure. In this framework we define a proof-relevant semantics: t
 he interpretation of a term associates to it the set of its typing derivat
 ions in appropriate systems. We prove that our model characterize solvabil
 ity\, adapting reducibility techniques to our setting. We conclude by desc
 ribing wo examples of our construction.\n
LOCATION:https://researchseminars.org/talk/itaca/12/
END:VEVENT
END:VCALENDAR