Published: 7th February 2017 DOI: 10.4204/EPTCS.242 ISSN: 2075-2180 |
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 |
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 wereI 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
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.
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