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


Manage episode 282562362 series 2823367
著作 Aaron Stump の情報はPlayer FM及びコミュニティによって発見されました。著作権は出版社によって所持されます。そして、番組のオーディオは、その出版社のサーバから直接にストリーミングされます。Player FMで購読ボタンをタップし、更新できて、または他のポッドキャストアプリにフィードのURLを貼り付けます。

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 つのエピソード