Alex Simpson: Relational parametricity for polymorphic lambda-calculus

Datum objave: 2. 11. 2015
Seminar za temelje matematike in teoretično računalništvo
Torek, 3. 11. 2015, od 12h do 14h, Plemljev seminar, Jadranska 19
Abstract: Two weeks ago, I reviewed the polymorphic lambda-calculus, introduced independently by Girard (as "System F") and Reynolds in the early 1970s, focusing in particular on its syntax and on its category-theoretic models. This week I shall discuss how "relational parametricity" allows one to establish strong properties of the calculus. This will be addressed via the introduction of a type theory for relational parametricity, and its category-theoretic semantics. This is once again joint work with Neil Ghani and Fredrik Nordvall Forsberg of the University of Strathclyde.