**( news )**

**Previous Presentations**

- Bob Coyne on Words Eye
- Brandon Bloom on Term Rewriting

**Upcoming Events**

- Gershom Bazerman on Homotopic Type Theory
- RPL on Prolog and Core Logic
- Lisp Summer BBQ

**( news )**

**Previous Presentations**

- Bob Coyne on Words Eye
- Brandon Bloom on Term Rewriting

**Upcoming Events**

- Gershom Bazerman on Homotopic Type Theory
- RPL on Prolog and Core Logic
- Lisp Summer BBQ

**( meeting - Tuesday, May 12, 7:00 PM - 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 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” [1] 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 [2], 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.

[1] http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf

[2] http://homotopytypetheory.org/book/

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.

Location:

Google

76 9th Ave. 4th Floor

You must RSVP here or at Meetup

**( news stream )**

LispNYC is a nonprofit unincorporated association dedicated to the advocacy and advancement of Lisp-based software and development technologies such as Common Lisp, Clojure and Scheme.

We focus on **education, outreach**, regular **monthly meetings** and development projects.

Meetings are the second Tuesday of every month, are free and open to all.

*Providing parentheses to NYC since 2002*