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 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.
A dependent type theory can also be thought of as a programming language, and the system we develop, following Martin-Löf’s 1979 “Constructive Mathematics and Computer Programming”  can be thought of as a “little language” embedded in Scheme that comes with a system of judgments by which we can verify properties of our programs, and which includes a foreign function interface to the whole of mathematics.
We will point towards some questions that immediately arise when asking “what does it mean for some value to be equal to some other value” and “what does it mean for some type to be equal to some other type,” and consider some of the approaches to answering these sorts of questions. This invariably leads to the Univalence Axiom -- the proposition that equality is equivalent to equivalence.
We will then proceed to a sketch of the homotopy interpretation of type theory , in which the univalence axiom is validated. Finally, we will conclude some ideas of how we can understand the homotopy interpretation (and implement it) in light of the system presented.
The talk will be conducted using the racket variant of the Scheme language, making frequent use of pattern matching.
Biography: Gershom Bazerman is an organizer of the NY Haskell Users Group and the NY Homotopy Type Theory Reading Group, which has now been studying Homotopy Type Theory for over a year. He has given a fair number of talks on programming and mathematics, and enjoys trying to make apparently complicated things understandable.