Parametric models and representation independence

Iowa Type Theory Commute

Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence. This is a feature of a type theory where different implementations of the same interface can be proved equivalent, and used interchangeably in the theory. Only in the past couple years have researchers proposed theories like this, but the semantic ideas underlying such theories have been around since Reynolds's seminal paper "Types, Abstraction, and Parametric Polymorphism".