Warning: Table './church/sessions' is marked as crashed and last (automatic?) repair failed query: SELECT sid FROM sessions WHERE sid = 'flahhete8tmneh803bu62j2ta0' in /var/www/church/includes/database.mysql.inc on line 121
Gruppo di Logica e Geometria della Cognizione
Year | Month | Week | Day
« prevVenerdì, Gennaio 15 2021next »
Key 1

Intersection Type Distributors

Speaker:
Federico Olimpieri
Quando:
15/01/2021 - 15:00
Dove:
Videoconferenza su teams al link https://bit.ly/3bbdIMz
Abstract

Building on previous works, we present a general method to define proof relevant intersection type semantics for pure lambda calculus. We argue that the bicategory of distributors is an appropriate categorical framework for this kind of semantics. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management, following Marsden-Zwardt's approach. We show how these monadic constructions determine Kleisli bicategories over the bicategory of distributors and we give a sufficient condition for cartesian closedness. We define a family of non-extensional models for pure lambda calculus. We then prove that the interpretation of lambda terms induced by these models can be concretely described via intersection type systems. The intersection constructor corresponds to the particular tensor product given by the considered free monadic construction.



Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: SELECT sid FROM sessions WHERE sid = 'flahhete8tmneh803bu62j2ta0' in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/calendario/2021/01/15', '', '98.80.143.34', 1728494691) in /var/www/church/includes/database.mysql.inc on line 121

Warning: Can't find file: 'watchdog' (errno: 2) query: INSERT INTO watchdog (uid, type, message, severity, link, location, referer, hostname, timestamp) VALUES (0, 'php', 'Table './church/sessions' is marked as crashed and last (automatic?) repair failed\nquery: INSERT INTO sessions (sid, uid, cache, hostname, session, timestamp) VALUES ('flahhete8tmneh803bu62j2ta0', 0, 0, '98.80.143.34', 'calendar_year|i:2021;calendar_mon|i:1;', 1728494691) in /var/www/church/includes/database.mysql.inc on line 121.', 2, '', 'http://logica.uniroma3.it/calendario/2021/01/15', '', '98.80.143.34', 1728494691) in /var/www/church/includes/database.mysql.inc on line 121