Podcasts Technology Iowa Type Theory Commute On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler

On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler

Published: Jan. 18, 2021, 6 a.m.

b'

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.\\xa0 RelTT uses a generalization of these ideas to derive induction for any positive type family.

'