From Scheme to Dependent Type Theory in 100 Lines

0 0

In this talk we will introduce Dependent Type Theory through the one of the typically nicest ways to understand anything at all — implementing it in Scheme! As it turns out, the untyped lambda calculus provides excellent raw material over which to construct a proof theory, based on the notion that a proposition may be verified through the construction of a lambda-term which realizes its meaning.

Gershom Bazerman on "From Scheme to Dependent Type Theory in 100 Lines"

From Scheme to Dependent Type Theory in 100 Lines a.k.a. Lambda: The Ultimate Realizer a.k.a. Homotopy Spaces: The Ultimate Extensional Realizer? In this talk we will introduce Dependent Type Th...