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 JanDisplayed time zone: Tijuana, Baja California change
Wed 10 Jan
Displayed time zone: Tijuana, Baja California change
10:30 - 12:10 | Types and EffectsResearch Papers at Watercourt Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge | ||
10:30 25mTalk | Linear Haskell: practical linearity in a higher-order polymorphic language Research Papers Jean-Philippe Bernardy University of Gothenburg, Mathieu Boespflug Tweag I/O, Ryan R. Newton Indiana University, Simon Peyton Jones Microsoft Research, Arnaud Spiwack Tweag I/O Pre-print File Attached | ||
10:55 25mTalk | Polyadic Approximations, Fibrations and Intersection Types Research Papers | ||
11:20 25mTalk | Handling fibred algebraic effects Research Papers Danel Ahman Inria Paris | ||
11:45 25mTalk | Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Research Papers Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław |