The intersection-types discipline for λ-calculus was introduced in Coppo and Dezani-Ciancaglini (1980) as an extension of Curry's type assignment system. The motivation was essentially to increase the class of terms possessing types. Indeed, it turned out that this discipline can assign types to all and only the strongly normalising terms. This is largely a folklore result; the first published proof appears in Pottinger (1980). Subsequently, the intersection-types discipline was used in Barendregt et al. (1983) as a tool for proving Scott's conjecture concerning the completeness of the set-theoretic semantics for simple types.

The purpose of this note is to give a methodologically simple proof of the undecidability of strong normalisation in the pure lambda calculus. For this we show how to represent an arbitrary partial recursive function by a term whose application to any Church numeral is either strongly normalizable or has no normal form. Intersection types are used for the strong normalization argument.

This paper presents a novel method for comparing computational properties of λ-terms that are typeable with intersection types, with respect to terms that are typeable with Curry types. We introduce a translation from intersection typing derivations to Curry typeable terms that is preserved by β-reduction: this allows the simulation of a computation starting from a term typeable in the intersection discipline by means of a computation starting from a simply typeable term. Our approach proves strong normalisation for the intersection system naturally by means of purely syntactical techniques. The paper extends the results presented in Bucciarelli et al. (1999) to the whole intersection type system of Barendregt, Coppo and Dezani, thus providing a complete proof of the conjecture, proposed in Leivant (1990), that all functions uniformly definable using intersection types are already definable using Curry types.

This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction.

We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.

We show how the principal typing property of the rank 2 intersection type system enables the specification of a modular and polyvariant control-flow analysis.

We present a type-based flow analysis for simply typed lambda calculus with booleans, data-structures and recursion. The analysis is exact in the following sense: if the analysis predicts a redex, there exists a reduction sequence (using standard reduction plus context propagation rules) such that this redex will be reduced. The precision is accomplished using intersection typing.

It follows that the analysis is non-elementary recursive – more surprisingly, the analysis is decidable. We argue that the specification of such an analysis provides a good starting point for developing new flow analyses and an important benchmark against which other flow analyses can be compared. Furthermore, we believe that the techniques employed for stating and proving exactness are of independent interest: they provide methods for reasoning about the precision of program analyses.

A preliminary version of this paper has previously been published (Mossin 1997b). The present paper extends, elaborates and corrects this previously published abstract.

We investigate the use of conjunctive non-standard type inference for the elimination of useless code in higher-order typed functional programs. In particular, we present a non-standard type assignment system for detecting useless code together with a mapping that simplifies a program by removing the useless code detected using the system.