Intersection Types for Normalization and Verification

摘要

One of the basic principles in typed lambda calculi is that typable lambda terms are normalizable. Since the converse direction does not hold for simply typed lambda calculus, people have been studying its extensions. This gave birth to the intersection type systems, that exactly characterize various classes of lambda terms, such as strongly/weakly normalizable terms and solvable ones(see e.g. [6] for a survey). More recently, a new trend has emerged: intersection types are not only useful for extending simple types but also for refining them [4]. One thus obtains finer information on simply typed terms by assigning intersection types. This in particular leads to the concept of normalization by typing, that turns out to be quite efficient in some situations [5]. Moreover, intersection types are invariant under β-equivalence, so that they constitute a denotational semantics in a natural way [1]. Finally, intersection types also work in an infinitary setting, where terms may represent infinite trees and types play the role of automata. This leads to a model checking framework for higher order recursion schemes via intersection types [2, 3]. The purpose of this talk is to outline-the recent development of intersection types described above. In particular, we explain how an efficient evaluation algorithm is obtained by combining normalization by typing, β-reduction and Krivine's abstract machine, to result in the following complexity characterization. Consider simply typed lambda terms of boolean type o → o → o and of order r. Then the problem of deciding whether a given term evaluates to "true" is complete for n-EXPTIME if r = 2n + 2, and complete for n-EXPSPACE if r = 2n + 3 [5].