Schedule of ITRS'08 meeting - Turin, March 25th, 2008


Intersection type assignment systems for intuitionistic sequent calculus
José Espirito Santo, Jelena Ivetic and  Silvia Likavec

We present and analyse various intersection type assignment systems for the  λGtz calculus, a calculus that embodies the Curry-Howard
correspondence for intuitionistic sequent calculus. Three systems  λGtz I,  λGtz Io  and λGtz I# successfully characterise the strongly normalising terms in λGtz. The first one  is presented as a refinement of two previous, unsuccessful attempts. The latter two try to reduce to a minimum the use of the meta-level type equivalence. The management of intersection is, in all successful  systems, built in the ordinary logical rules.

Realisability Semantics for Intersection Types and Expansion Variables
Fairouz Kamareddine, Karim Nour, Vincent Rahli and Joe Wells

Expansion was invented at the end of the 1970s for calculating principal typings for lambda-terms in type systems with intersection types.  Expansion variables (E-variables) were invented at the end of the 1990s to simplify and help mechanize expansion.  Recently, E-variables have been further simplified and generalized to also allow calculating other type operators than just intersection.  There has been much work on denotational semantics for type systems with intersection types, but none whatsoever before now on type systems with E-variables. Building a semantics for E-variables turns out to be challenging. To simplify the problem, we consider only E-variables, and not the corresponding operation of expansion. We develop a realizability semantics where each use of an E-variable in a type corresponds to an independent level at which evaluation occurs in the lambda-term that is assigned the type. In the lambda-term being evaluated, the only interaction possible between portions at different levels is that higher level portions can be passed around but never applied to lower level portions.  We apply this semantics to two intersection type systems.  We show these systems are sound, that completeness does not hold for the first system, and completeness holds for the second system when only one E-variable is allowed (although it can be used many times and nested). As far as we know, this is the first study of a denotational semantics of intersection type systems with E-variables (using realizability or any other approach) and of the difficulties involved.

Reducibility proofs in lambda-calculi with intersection types
Fairouz Kamareddine, Vincent Rahli and Joe Wells

Reducibility has been used to prove a number of properties in the lambda-calculus and is well known to offer on one hand very general proofs which can be applied to a number of instantiations, and on the other hand, to be quite mysterious and inflexible. In this paper, we look at two related but different results in lambda-calculi with intersection types. We show that one such result (which aims at giving reducibility proofs of Church-Rosser, standardization and weak normalisation) faces serious problems which break the reducibility method and then we provide a proposal to partially repair the method. Then, we consider a second result whose purpose is to use reducibility to show Church-Rosser of beta-developments (without needing to use strong normalisation). We extend the second result to encompass both beta I- and beta eta-reduction rather than simply beta-reduction.

Strong normalization in the π-calculus with intersection and union types
Mauro Piccolo

We present a typing system for the  π-calculus which guarantees that every well-typed term is strongly normalizing. Our typing system is an extension of that presented by Yoshida, Berger, Honda (2004) and it is able to type more term than that presented there.

Intersection Types: a Proof-Theoretical Approach
Elaine Pimentel, Simona Ronchi della Rocca and Luca Roversi

In this work we present a proof-theoretical justification for IT by means of the logical system Intersection Synchronous Logic (ISL). ISL builds equivalence classes of deductions of the implicative and conjunctive fragment of NJ. ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous conjunction, that can be used only among equivalent deductions of NJ, and an asynchronous one, that can be applied among any sets of deductions of NJ. A term decoration of ISL exists so that it matches both: the IT assignment system, when only the synchronous conjunction is used, and the simple types assignment with pairs and projections, when the asynchronous conjunction is used. Moreover, the proof of strong normalization property for ISL is a simple consequence of the same property in NJ and hence strong normalization for IT comes for free.

Towards an intersection and union logic
Anastasia Veneti and Yiorgos Stavrinos

A logical foundation for the intersection and union types assignment system (IUT) is proposed. We present Intersection-Union Logic (IUL) as an extension of Intersection Logic (IL) by adding rules for union and we examine some properties of this system and its relation with intuitionistic minimal logic.

The Algebra of Expansion
Sébastien Carlier and Joe Wells

Expansion is an operation on typings (pairs of type environments and result types) in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a term in systems with intersection types. Unfortunately, definitions of expansion (even the most modern ones) have been difficult for outsiders to absorb. This paper aims to clarify expansion and make it more accessible to non-specialists by isolating the pure notion of expansion on its own. We show how expansion can be seen as a simple algebra on terms with variables, substitutions, composition, and miscellaneous constructors such that the algebra satisfies 8 simple equalities: the 3 standard equalities of a monoid, 4 standard equalities of substitutions (including one that corresponds to the usual “substitution lemma”), and 1 equality for expansion itself. This presentation should help make more accessible to a wider community theory and techniques involving intersection types and type inference with flexible precision.

Reduction in X does not agree with Intersection and Union Types
Steffen van Bakel

This paper will present a notion of intersection and union type assignment for the (untyped) calculus X, as first defined in (Lengrand'03) and later extensively studied in (van Bakel-Lengrand-Lescanne'05). X is based on the sequent calculus (Gentzen'35), in contrast to the Lambda Calculus (Barendregt'84) which is based on natural deduction (see also (Gentzen'35)); the advantage of using the sequent approach in this paper is that now we can study and explain various anomalies of union type assignment (Barbanera-Dezani-Liguoro-IaC'95) and quantification (Harper-Lillibridge'91,'97).
The type system defined here initially will be shown to be the natural one, in that intersection and union play their expected roles for \emph{witness expansion} (also called \emph{completeness}). However, we show that \emph{witness reduction} (also called \emph{soundness}, the converse of completeness) no longer holds, and will reason that this is caused by the non-logical foundation of both intersection and union. This problem also appears in other contexts, such as that of ML with side-effects (Harper-Lillibridge'91,Wright'95,'97), and that of using intersection and union types in an operational setting (Davies-Pfenning'01,Dunfield-Pfenning'00). As here, also there the cause of the problem is the lack of accompanying syntax for the added type constructors, making the non-standard reductions (essentially context calls, which form part of the reduction in X) unsafe. As, in part, already been observed in (Herbelin'05) in the context of the calculus  λμμ~ of (Curien-Herbelin'00), the problem is that the added rules are not logical.
The advantage of studying this problem in the context of the highly symmetric sequent calculi will be made clear: intersection and union are truly dual for these calculi, and the at the time surprising loss of soundness for the system with intersection and union types in (Barbanera-Dezani-Liguoro-IaC'95) becomes now natural and inevitable. Also, we will show that it is not union alone that causes problems, but that the problem is much more profound: although the idea behind both intersection and union might be the (logical) \emph{and} and \emph{or}, the fact that they are both \emph{not} logical (Hindley'84) destroys the soundness, both for a system based on intersection, as for a system based on union. This also explains why, for ML with side-effects, quantification is no longer sound (Harper-Lillibridge'91,'97): also the (∀ I) and (∃ E) rules of ML are not logical.
This paper is constructed as follows. Section 1 presents the syntax and reduction system of the calculus X. In Section 2 we define the basic system of context assignment for X; in Section 3 we will embed the Lambda Calculus into X, and present an Intersection System for the LC. Then, in Section 4, we will define a notion of type assignment on X that uses intersection and union types, and show that type assignment in the strict system is preserved by the translation of the Lambda Calculus into X.