<p>I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent.  This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.</p>

I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent. This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.

<p>I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent.&nbsp; This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.</p>

Equivalence of inductive and parametric naturals in RelTT

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share Equivalence of inductive and parametric naturals in RelTT

Sign up to save your podcasts

Equivalence of inductive and parametric naturals in RelTT

Equivalence of inductive and parametric naturals in RelTT