On the paper "Types, Abstraction, and Parametric Polymorphism"
In this episode I discuss one of the greatest papers in the history of Programming Language's research, namely "Types, Abstraction, and Parametric Polymorphism" by the great John C. Reynolds. I summarize the two interconnected semantics for polymorphic types proposed by Reynolds: one which interprets types as sets and programs as members of those sets, and another which interprets types as relations on the sets from the first interpretation. Listen and you will get to hear my aha moment as I understand live on air what the Identity Extension Lemma really means. See also this blog post on the same topic.
The podcast Iowa Type Theory Commute is embedded on this page from an open RSS feed. All files, descriptions, artwork and other metadata from the RSS-feed is the property of the podcast owner and not affiliated with or validated by Podplay.