|
Published: 21st January 2011 DOI: 10.4204/EPTCS.45 ISSN: 2075-2180 |
| Preface Elaine Pimentel, Betti Venneri and Joe Wells | |
| Invited Presentation: Relating Church-Style and Curry-Style Subtyping Adriana Compagnoni and Healfdene Goguen | 1 |
| Invited Presentation: Intersection Logic in sequent calculus style Simona Ronchi Della Rocca, Alexis Saurin, Yiorgos Stavrinos and Anastasia Veneti | 16 |
| Sound and Complete Typing for lambda-mu Steffen van Bakel | 31 |
| Intersection types for unbind and rebind Mariangiola Dezani-Ciancaglini, Paola Giannini and Elena Zucca | 45 |
| Untangling Typechecking of Intersections and Unions Joshua Dunfield | 59 |
| Session Types = Intersection Types + Union Types Luca Padovani | 71 |
| Equality, Quasi-Implicit Products, and Large Eliminations Vilhelm Sjöberg and Aaron Stump | 90 |
This volume contains the final and revised versions of the papers presented at the Fifth Workshop on Intersection Types and Related Systems (ITRS 2010). The workshop was held in Edinburgh, U.K. on July 9, 2010, as part of FLoC and affiliated with LICS 2010. The aim of the ITRS workshop series is to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches (e.g., union types, refinement types, behavioral types).
Intersection types were introduced near the end of the 1970s to overcome the limitations of Curry’s type assignment system and to provide a characterization of the strongly normalizing terms of the Lambda Calculus. The key idea is to introduce an intersection type constructor ^ such that a term of type t^s can be used at both type t and s within the same context. This provides a finite polymorphism where various, even unrelated, types of the term are listed explicitly, differently from the more widely used for-all-quantified types where the polymorphic type is the common schema which stands for its various type instances. As a consequence, more terms (all and only the normalizing terms) can be typed than with universal polymorphism. Intersection types have been one of the first examples of behavioral type theory: they provide an abstract specification of computational properties, by expressing a finer and more precise input/output relation than standard, commonly used, type systems can do.
Although intersection types were initially intended for use in analyzing and/or synthesizing lambda models as well as in analyzing normalization properties, over the last twenty years the scope of the research on intersection types and related systems has broadened in many directions. Restricted (and more manageable) forms have been investigated, such as refinement types. Type systems based on intersection type theory have been extensively studied for practical purposes, such as program analysis. The dual notion of union types turned out to be quite useful for programming languages. Finally, the behavioral approach to types, which can give a static specification of computational properties, has become central in the most recent research on type theory.
The invited speakers at ITRS 2010 were
Adriana Compagnoni (Stevens Inst. of Technology, New-Jersey)
Simona Ronchi Della Rocca (Univ. di Torino)
The program committee of ITRS 2010 consisted of
Betti Venneri (Univ. di Firenze) Chair
Mariangiola Dezani-Ciancaglini (Univ.di Torino)
Joshua Dunfield (McGill University, Montreal)
Silvia Ghilezan (Univ. of Novi Sad)
Atsushi Igarashi (Kyoto University)
Elaine Pimentel (Univ.of Belo Horizonte)
Joe Wells (Heriot-Watt University, Edinburgh)
The papers were refereed by the program committee and by the following outside referees, whose help is gratefully acknowledged: Fabio Alessi, Franco Barbanera, Koji Nakazawa, Ferruccio Damiani, Paola Giannini.
Elaine Pimentel, Betti Venneri and Joe Wells