|Time:|| 12:30 - 13:50
Wean Hall 8220
Department of Mathematical Sciences
Carnegie Mellon University
Polymorphism and self-application
System F is a system of parametric polymorphism that corresponds to second order propositional logic. As a system of typed λ-calculus, it has the strong normalization property (where not all such terms are typed) and types all normal forms. These imply that some β-expansions fail. In this talk we will explore the properties of this system and give some partial results regarding the question of ω (λx.xx) expansions.