Dependent types are showing up in more and more mainstream languages, but they can still seem like magic. In this workshop, we'll walk through one of the primary techniques for implementing a type checker for dependent types, called normalization by evaluation. We'll be implementing a little dependently typed language called Pie developed by Dan Friedman and myself.
The implementation is written entirely in a very small subset of Scheme, and I'll assume no knowledge beyond that gained by reading The Little Schemer.
* Introduce the ideas behind normalization by evaluation and
bidirectional type checking
* Write a type checker for a little dependently typed language
* Basic familiarity with and interest in dependent types, equivalent
to having worked through the Idris tutorial 
* Know enough Racket or Scheme to write an interpreter for a small
* Have a recent version of Racket installed on your laptop
Dependent types let us use the same programming language for compile-time and run-time code, and are inching their way towards the mainstream from research languages. Unfortunately, the essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools.
Pie is a little dependently typed language, small enough to understand completely but big enough to write a variety of proofs and programs.
Come get a taste of Pie, and see for yourself where dependent types can take us.
* Convey the core ideas of propositions as types, proofs as programs
* Show the off the wonder and magic of dependent types in Pie
* Anyone who is comfortable with parentheses and recursion
David works at the border between type theory and type practice. He has done work on Idris, especially its interactive environment and metaprogramming facilities, and is currently working on integrating proofs and macros in Racket.