ITRS on Friday, July 9th

09:00‑10:00 Invited talk
Chair: Betti Venneri
Location: AT 2.11
09:00 Adriana Compagnoni (Stevens Inst. of Technology)
Relating Church-style and Curry-style Subtyping
10:30‑11:30 Session Types
Chair: Joe Wells
Location: AT 2.11
10:30 Luca Padovani
Session Types = Intersection Types + Union Types

We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories.

11:00 Elena Giachino
On Semantic Subtyping and Safe Object-Oriented Sessions

Agents willing to safely exchange messages must agree on a protocol to adopt during the interaction, to be guaranteed that the communication proceeds without mismatches. In the theory of session types the specification of the protocol is a type associated to the communication channel.

A semantic subtyping framework for session types has been proposed by Castagna et al., providing a way for any language with sessions and communication primitives to adopt session types without modifying them to fit in the specific language.

In this paper we show how to exploit the semantic framework to obtain safe session communications in an object-oriented calculus, enabling session overloading. We demonstrate our ideas through a calculus formalizing the main issues of the present approach. Our calculus is proven to be type safe: the evaluation of a well-typed executable program cannot get stuck on a communication deadlock.

11:30‑12:30 Program Properties
Chair: Mariangiola Dezani-Ciancaglini
Location: AT 2.11
11:30 Joshua Dunfield
Untangling Typechecking of Intersections and Unions

Intersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics. Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into let-normal form drastically reduces the number of choices. The key results are soundness and completeness: a typing derivation (in the system with too many subterm choices) exists for a program if and only if a derivation exists for the let-normalized program.

12:00 Vilhelm Sjöberg and Aaron Stump
Equality, Quasi-Implicit Products, and Large Eliminations

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the metatheory for an undecidable version of the system with unannotated terms. We then devise a decidable system with annotated terms, justified in terms of the unannotated system. Finally, we show how the approach can be extended to account for large eliminations, using what we call quasi-implicit products.

14:00‑15:00 Invited talk
Chair: Silvia Ghilezan
Location: AT 2.11
14:00 Simona Ronchi Della Rocca (Univ. of Torino)
Intersection and Union Logic
15:30‑16:30 Extended Lambda Calculus
Chair: Joshua Dunfield
Location: AT 2.11
15:30 Steffen van Bakel
Sound and Complete Typing for Lambda-Mu

In this paper we define intersection and union type assignment for Parigot's calculus Lambda-Mu. We show that this notion is complete (i.e. closed under subject-expansion), and show also that it is sound (i.e. closed under subject-reduction). This implies that this notion of intersection-union type assignment is suitable to define a semantics.

16:00 Paola Giannini, Mariangiola Dezani-Ciancaglini and Elena Zucca
Intersection types for unbind and rebind (Extended Abstract)

We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term $e$ with free variables $x_1,\ldots,x_n$, representing open code, can be packed into an \emph{unbound} term $<x_1,\ldots,x_n | e>$, and passed around as a value. In order to execute inside code, an unbound term should be explicitly \emph{rebound} at the point where it is used. Unbinding and rebinding are hierarchical, that is, the term $e$ can contain arbitrarily nested unbound terms, whose inside code can only be executed after a sequence of rebinds has been applied. Correspondingly, types are decorated with levels, and a term has type $\tau^k$ if it needs $k$ rebinds in order to reduce to a value of type $\tau$. With intersection types we model the fact that a term can be used differently in contexts providing a different numbers of unbinds. In particular, top-level terms, that is, terms not requiring unbinds to reduce to values, should have a \emph{value} type, that is, an intersection type where at least one element has shape $\tau^0$. With the proposed intersection type system we get soundness w.r.t the call-by-value strategy, an issue which was not resolved by previous type systems.