Alex Simpson: Polymorphic lambda-calculus

Abstract: I shall review some of the properties of the polymorphic lambda-calculus, introduced independently by Girard (as "System F") and Reynolds in the early 1970s. In the seminar, I will focus on three things: (i) the syntax of the calculus; (ii) its surprising programming power; and (iii) its category-theoretic semantics. Regarding (iii), I shall present a modification of the usual notion of model, which will be needed in a follow-up seminar on relational parametricity. Part (iii) is joint work with Neil Ghani and Fredrik Nordvall Forsberg of the University of Strathclyde.