Wed 10 Jan 2018 10:55 - 11:20 at Watercourt - Types and Effects Chair(s): Neel Krishnaswami

Starting from an exact correspondence between affine approximations and non-idempotent intersection types, we develop a general framework for building intersection types systems characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger’s ``type systems as functors'' viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani’s original system, as well as its non-idempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way.

Wed 10 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

10:30 - 12:10: Research Papers - Types and Effects at Watercourt
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge
POPL-2018-papers10:30 - 10:55
Jean-Philippe BernardyUniversity of Gothenburg, Mathieu BoespflugTweag I/O, Ryan R. NewtonIndiana University, Simon Peyton JonesMicrosoft Research, Arnaud SpiwackTweag I/O
Pre-print File Attached
POPL-2018-papers10:55 - 11:20
POPL-2018-papers11:20 - 11:45
Danel AhmanInria Paris
POPL-2018-papers11:45 - 12:10
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław