[PL-sem-jr] Talk Monday, 2/2: Jed on undecidability of bounded quantification

[Aaron Turon]

The abstract for Benjamin Pierce's 1992 paper, "Bounded quantification
is undecidable", which Jed will be presenting on 2/2:

"F≤ is a typed lambda-calculus with subtyping and bounded second-order
polymorphism. First proposed by Cardelli and Wegner, it has been
widely studied as a core calculus for type systems with subtyping.
Curien and Ghelli proved the partial correctness of a recursive
procedure for computing minimal types of F≤ terms and showed that the
termination of this procedure is equivalent to the termination of this
procedure is equivalent to the termination of its major component, a
procedure for checking the subtype relation between F≤ types. This
procedure was thought to terminate on all inputs, but the discovery of
a subtle bug in a purported proof of this claim recently reopened the
question of the decidability of subtyping, and hence of typechecking.
This question is settled here in the negative, using a reduction from
the halting problem for two-counter Turing machines to show that the
subtype relation of F≤ is undecidable."

On Sun, Feb 1, 2009 at 3:08 PM, Aaron Turon <turon at ccs.neu.edu> wrote:
> Tomorrow, 2/2 at 2:30 in WVH166.
>
> Jed will discuss the undecidability of bounded quantification (in type
> systems: think system F_<:).  Talk abstract will appear in follow-up
> email.
>
> --
>
> Upcoming schedule:
> 2/9 Aaron - nominal logic
> 2/16 Holiday (President's day)
> 2/23 Dimitris - control-flow analysis
>