Published: 17th March 2015
DOI: 10.4204/EPTCS.177
ISSN: 2075-2180

EPTCS 177

Proceedings Seventh Workshop on
Intersection Types and Related Systems
Vienna, Austria, 18 July 2014

Edited by: Jakob Rehof
Preface
Jakob Rehof
A Finite Model Property for Intersection Types
Rick Statman		1
Uniform Proofs of Normalisation and Approximation for Intersection Types
Kentaro Kikuchi		10
Liquid Intersection Types
Mário Pereira, Sandra Alves and Mário Florido		24
Indexed linear logic and higher-order model checking
Charles Grellois and Paul-André Melliès		43
On Isomorphism of "Functional" Intersection and Union Types
Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria and Maddalena Zacchi		53
Lucretia — intersection type polymorphism for scripting languages
Marcin Benke, Viviana Bono and Aleksy Schubert		65
Typing Classes and Mixins with Intersection Types
Jan Bessai, Boris Düdder, Andrej Dudenhefner, Tzu-Chun Chen and Ugo de'Liguoro		79

Preface

This volume contains a final and revised selection of papers presented at the Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), held in Vienna (Austria) on July 18th, affiliated with TLCA 2014, Typed Lambda Calculi and Applications (held jointly with RTA, Rewriting Techniques and Applications) as part of FLoC and the Vienna Summer of Logic (VSL) 2014.

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 have 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, and program synthesis.

The aim of the ITRS workshop series [6, 1, 2, 3, 5, 4] 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).

The members of the ITRS 2014 Program Committee were

I wish to express my gratitude to authors, Program Committee members, referees, the Steering Commitee and all people who supported the publication of these post-Proceedings, including Boris Düdder, Rocco De Nicola, Mariangiola Dezani, Moritz Martens, and Luca Paolini.

Jakob Rehof
Technical University of Dortmund
jakob.rehof@cs.tu-dortmund.de

References

  1. Steffen van Bakel (2002): Proceedings of the Second International Workshop on Intersection Types and Related Systems. 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 Systems. Electronic Notes in Theoretical Computer Science 136. Colocated with the joint meeting of ICALP 2004 and LICS 2004 in Turku, Finland, doi:10.1016/j.entcs.2005.06.018.
  3. Silvia Ghilezan & Luca Paolini (2012): Proceedings of the Fourth International Workshop on Intersection Types and Related Systems. Fundamenta Informaticae 121(1-274). Colocated with TYPES 2008 in Torino, Italy, doi:10.3233/FI-2012-769.
  4. Stéphane Graham-Lengrand & Luca Paolini (2013): Proceedings of the Sixth InternationalWorkshop on Intersection Types and Related Systems. Electronic Proceedings in Theoretical Computer Science 121. Colocated with the Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012) in Dubrovnik, Croatia, doi:10.4204/EPTCS.121.
  5. Elaine Pimentel, Betti Venneri & Joe Wells (2010): Proceedings of the Fifth International Workshop on Intersection Types and Related Systems. Electronic Proceedings in Theoretical Computer Science 45 (1-100). Colocated with LICS 2010 (as part of FLoC 2010) in Edinburgh, Scotland, doi:10.4204/EPTCS.45.
  6. Joe Wells (2000): Proceedings of the First International Workshop on Intersection Types and Related Systems. Colocated with ICALP 00, the 27th International Colloquium on Automata, Languages, and Programming in Geneva, Switzerland.