------------------------------------------------------------------------------- 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 25, 1994 3:00pm (Coffee served at 2:30pm) Seminar Room / MCS 135 ------------------------------------------------------------------------------- Type Inference within the Polymorphically-Typed Lambda Calculus Joe Wells Boston University ABSTRACT Typed lambda calculi interest both designers of computer programming languages and logicians. On the programming language side, various functional programming languages (ML, Haskell, Miranda, QUEST, LEAP, etc.) use typed lambda calculi for their foundations. On the logic side, each typed lambda calculus corresponds directly to some calculus of logic. One particular typed lambda calculus, the second-order, polymorphically-typed lambda calculus, was invented independently by Reynolds, a programming language designer, and Girard, a logician. We use this calculus's short name, system F. Solutions to the closely related problems of type inference, typability, and type-checking have been pursued for over a decade for system F. Research has also considered restrictions and extensions of system F. This talk presents the recent result that typability and type-checking are undecidable for system F, which implies that type inference is impossible for system F. This talk also discusses a fragment of system F for which type inference is possible and how to carry out this task. This talk will include a brief introduction to typed lambda calculi. Host: Prof. Assaf Kfoury ------------------------------------------------------------------------------- For more information contact Prof. Azer Bestavros . -------------------------------------------------------------------------------