Published: 30th July 2013
DOI: 10.4204/EPTCS.121
ISSN: 2075-2180

EPTCS 121

Proceedings Sixth Workshop on
Intersection Types and Related Systems
Dubrovnik, Croatia, 29th June 2012

Edited by: Stéphane Graham-Lengrand and Luca Paolini

Preface
Stéphane Graham-Lengrand and Luca Paolini
Characterisation of Strongly Normalising lambda-mu-Terms
Steffen van Bakel, Franco Barbanera and Ugo de'Liguoro
1
Using Inhabitation in Bounded Combinatory Logic with Intersection Types for Composition Synthesis
Boris Düdder, Oliver Garbe, Moritz Martens, Jakob Rehof and Paweł Urzyczyn
18
Annotations for Intersection Typechecking
Joshua Dunfield
35
Bounding normalization time through intersection types
Erika De Benedetti and Simona Ronchi Della Rocca
48
Toward Isomorphism of Intersection and Union types
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria and Maddalena Zacchi
58
Reconciling positional and nominal binding
Davide Ancona, Paola Giannini and Elena Zucca
81

Preface

This volume contains a final and revised selection of paper presented at the Sixth Workshop on Intersection Types and Related Systems (ITRS 2012), held in Dubrovnik (Croatia) the June 29th, affiliated with LICS 2012. Intersection types have been introduced in the late 1970s as a language for describing properties of lambda calculus which were not captured by all previous type systems. They provided the first characterisation of strongly normalising lambda terms and become a powerful syntactic and semantic tool for analysing various normalisation properties as well as lambda models. Over the years the scope of research on intersection types has broadened. Recently, there have been a number of breakthroughs in the use of intersection types and similar technology for practical purposes such as program analysis, verification and concurrency. The aim of the ITRS workshop series [5, 1, 2, 4, 3] 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).

Program Committee members of ITRS 2012 were composed by:

We express our gratitude to authors, referees, the Steering Commitee and all people who supported the publication of these post-Proceedings, Beniamino Accattoli, Alexis Bernadet, Ferruccio Damiani, Rocco De Nicola, Mariangiola Dezani-Ciancaglini, Dan Dougherty, Rob van Glabbeek, Stefan Monnier, Koji Nakazawa, Aleksandar Nanevski, Luca Padovani, Ivano Salvo, Paweł Urzyczyn, Pedro Vasconcelos, Joe Wells, Hongwei Xi.

Stéphane Graham-Lengrand
CNRS - École Polytechnique
graham-lengrand@lix.polytechnique.fr
Luca Paolini
Università di Torino, Dipartimento di Informatica
paolini@di.unito.it
(Editors of the issue)

References

[1]
Steffen van Bakel (2002): Proceedings of the Second International Workshop on Intersection Types and Related. Colocated with LICS 2002 (part of FLoC 2002) in Copenhagen, Denmark.
[2]
Mario Coppo & Ferruccio Damiani (2005): Proceedings of the Third International Workshop on Intersection Types and Related. Electronic Notes in Theoretical Computer Science 136, doi:10.1016/j.entcs.2005.06.018. Colocated with the joint meeting of ICALP 2004 and LICS 2004 in Turku, Finland.
[3]
Silvia Ghilezan & Luca Paolini (2012): Proceedings of Fourth International Workshop on Intersection Types and Related Systems. Fundamenta Informaticae 121(1-274), doi:10.3233/FI-2012-769. Colocated with TYPES 2008 in Torino, Italy.
[4]
Elaine Pimentel, Betti Venneri & Joe Wells (2010): Proceedings of Fifth International Workshop on Intersection Types and Related Systems. Electronic Proceedings in Theoretical Computer Science 45, pp. 1–100, doi:10.4204/EPTCS.45. Colocated with LICS 2010 (as part of FLoC 2010) in Edinburgh, Scotland.
[5]
Joe Wells (2000): Proceedings of the First International Workshop on Intersection Types and Related. Co-located with ICALP ’00, the 27th International Colloquium on Automata, Languages, and Programming in Geneva, Switzerland.