[PL-sem-jr] Talk tomorrow, Monday 11/9

[Aaron Turon]

Monday, 11/9, WVH164, 11:30-1:30

Speaker: Jed

Bounded Quantification is Undecidable

Once upon a time, there was a typed lambda calculus called System
$F_\le$. It had polymorphism (like System F) as well as subtyping, and
so was useful in reasoning about trendy new object-oriented languages.
 In 1990, Curien and Ghelli proved the partial correctness of a
recursive procedure for type-checking it; if the procedure terminated,
it would return the right answer.  They thought they'd also proved it
terminating... but they were wrong!  In fact, in 1992, Pierce proved
the problem of typechecking undecidable; or, put more excitingly, any
correct typechecker for $F_\le$ can be made to perform arbitrary
computation.

The proof is conveniently divided into a number of relatively simple
reductions, and along the way it explores the themes of manipulating
inductively defined judgments and performing computation on unlikely
substrates.