Mathematical logic seminar - August 26, 2014

Time: 12:30 - 13:50

Room: Wean Hall 8220

Speaker:     Will Gunther    
Department of Mathematical Sciences
Carnegie Mellon University

Title: 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.