------------------------------------------------------------------------------- B O S T O N U N I V E R S I T Y Computer Science Department C O L L O Q U I U M Wednesday, May 31, 1995 3:00pm (Coffee served at 2:45 pm) Seminar Room / MCS 135 ------------------------------------------------------------------------------- Non-Semantic Proofs of Strong Beta-Normalization in Typed Lambda Calculi Joe Wells Boston University An important question for any rewriting or reduction system is whether all rewrite or reduction sequences must terminate. It is well-known that the simply-typed lambda calculus and several standard polymorphic extensions (system F, the system of intersection types, and the system of positive recursive types) can only encode terms that strongly normalize (terminate) under beta reduction. Although this has been proven for the simply-typed lambda calculus in a variety of ways, prior to now all proofs for the polymorphic extensions have relied on the semantic methods introduced by Tait and refined by Girard. We present a non-semantic proof of strong normalization of beta reduction for the system of intersection types. First, we introduce another notion of reduction for lambda terms and convert the problem of strong normalization of beta reduction to the problem of weak normalization of the new reduction. Then, we prove weak normalization of this new reduction for the system of intersection types. Our method is closely related to a proof for the simply-typed lambda calculus by de Groote and has similarities to early proofs for the simply-typed lambda calculus by Nederpelt and Klop. ------------------------------------------------------------------------------- For colloquium info, including directions, see http://cs-www.bu.edu/colloquium For more information contact Prof. Mark Crovella -------------------------------------------------------------------------------