"A Little Taste of Dependent Types" by David Christiansen

David Christiansen introduces dependent types using the Pie programming language, demonstrating how types can express mathematical proofs.

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 like Coq, Agda and Idris. Dependent types are useful for programming, but they also unite programming and mathematical proofs, allowing us to use the tools and techniques we know from programming to do math. The essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools. The Little Typer is an upcoming book on dependent types in the tradition of the The Little Schemer that features a tiny dependently typed language called Pie. We will demonstrate a proof in Pie that is also a program. Come get a taste of Pie, and see for yourself where dependent types can take us. Speaker: David Christiansen