Intersection Types for Normalization and Verification (Invited Talk)

Abstract

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. [van Bakel/TCS/1995] 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 
[Salvati/JoLLI/2010]. 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 [Terui/RTA/2012]. Moreover, intersection types are invariant under beta-equivalence, so that they constitute a denotational semantics in a natural way [Ehrhard/CSL/2012]. 

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 [Kobayashi/POPL/2009, Kobayashi+Luke Ong/LICS/2009].
 
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, beta-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 [Terui/RTA/2012].