Published: 7th February 2017
DOI: 10.4204/EPTCS.242
ISSN: 2075-2180

EPTCS 242

Proceedings Eighth Workshop on
Intersection Types and Related Systems
Polto, Portugal, 26th June 2016

Edited by: Naoki Kobayashi

Preface
Naoki Kobayashi
Invited Talk: Intersection Types, Quantitative Semantics and Linear Logic
Michele Pagani
1
Invited Talk: Intersection Types for Real Number Computation
Kazushige Terui
2
Intersections and Unions of Session Types
Coşku Acay and Frank Pfenning
4
Characterisation of Approximation and (Head) Normalisation for λμ using Strict Intersection Types
Steffen van Bakel
20
Retractions in Intersection Types
Mario Coppo, Mariangiola Dezani-Ciancaglini, Alejandro Díaz-Caro, Ines Margaria and Maddalena Zacchi
31
Intersection Types and Related Systems
Paweł Parys
48

Preface

This volume contains a final and revised selection of papers presented at the Eighth Workshop on Intersection Types and Related Systems (ITRS 2016), held in Porto (Portugal) on June 26th, affiliated with FSCD 2016, 1st International Conference on Formal Structures for Computation and Deduction. The volume also contains the abstracts of two invited talks.

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 [7, 1, 2, 3, 5, 4, 6] 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 2016 Program Committee were

I wish to express my gratitude to invited speakers, authors, Program Committee members, referees, Steering Committee members and all people who supported the publication of these post-Proceedings, including Rocco De Nicola, Mariangiola Dezani, Jakob Rehof, and Joe Wells.

Naoki Kobayashi
The University of Tokyo
koba@is.s.u-tokyo.ac.jp

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 International Workshop 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. Jakob Rehof (2015): Proceedings of the Seventh International Workshop on Intersection Types and Related Systems. Electronic Proceedings in Theoretical Computer Science 177. Colocated with TLCA 2014 in Vienna, Austria, doi:10.4204/EPTCS.177.
  7. 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.

Intersection Types, Quantitative Semantics and Linear Logic

Michele Pagani (Université Paris Diderot)

Quantitative semantics refers to a family of semantics that interpret linear logic proofs as linear mappings between vector spaces (or more generally, modules), and standard lambda terms as power series. This idea has been used recently to give solid, denotational models for various algebraic extensions of lambda calculus, such as probabilistic and quantum lambda calculi. In this tutorial, we show how these models can be described via intersection types: a type corresponds to a vector of a canonical basis, and the interpretation of a term is computed according to the number of different type derivations associated with that term. As an instance, we show how this presentation has been used to prove the full abstraction of probabilistic coherence spaces for probabilistic PCF.


Intersection Types for Real Number Computation

Kazushige Terui (RIMS, Kyoto University, Japan)

There has been a trend of research which uses intersection types not for extending, but for refining simple types, which dates back to the 1990's but is most prominent in the last decade. According to this paradigm, one assigns intersection types to already simply typed lambda terms to reason about finer properties of programs and trees. It has been successfully applied in formal languages [5], in efficient evaluation of boolean-typed terms [6], and most importantly in model-checking of higher order recursion schemes [3].

A theoretical interest of this approach lies in its connection to denotational semantics of linear logic. For instance, the multiset-based relational semantics of linear logic corresponds to a system of nonidem- potent intersection types [1], while the Scott model of linear logic corresponds to a type system of [5]. The comonad in the latter can be combined with a coloring comonad [2], which semantically accounts for the type system of [3]. Such a connection with semantics not just backs up existing systems, but also motivates us to introduce new ones.

In our recent work with Kei Matsumoto, we have proposed a very simple and concrete interpretation of real numbers, functions and operators based on coherence spaces [4]. Specifically, we represent the real line by a coherence space R and build a typed realizability model upon it, according to which a real function is continuous if and only if it is realized by a stable map R ⇒ R. On the other hand, a real function is uniformly continuous if and only if it is realized by a linear map R -o R.

Now our idea is to convert coherence spaces to a type system. We consider a tiny programming language extending simply typed lambda calculus, in which computable real functions can be composed from primitive ones. We then introduce a system of coherent intersection types based on the above correspondence. It allows us to compositionally verify ε-δ-like properties of (uniformly) continuous functions. In this talk, we start by overviewing intersection types refining simple types in general, and then proceed to the above specific application for real number computation.

References

  1. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. Draft, 2009.
  2. Charles Grellois and Paul-Andre Mellies. Finitary semantics of linear logic and higher-order model- checking. In Proceedings of 40th MFCS, pages 256-268, 2015.
  3. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of 24th LICS, pages 179-188, 2009.
  4. Kei Matsumoto and Kazushige Terui. Coherence spaces for computable analysis. Presented at 12th CCA,2015.
  5. Sylvain Salvati. On the membership problem for non-linear abstract categorial grammars. Journal of Logic, Language and Information, 19(2):163-183, 2010.
  6. Kazushige Terui. Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In Proceedings of 23rd RTA, pages 323-338, 2012.