Parametric models and representation independence

Published: Nov. 9, 2020, 6 a.m.

b'

Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence.\\xa0 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.\\xa0 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".

'