## Iowa Type Theory Commute « » On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler

10:52

Manage episode 282562362 series 2823367

I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual type for Church-encoded natural numbers implies induction. RelTT uses a generalization of these ideas to derive induction for any positive type family.

128 つのエピソード