Thomas Dietert: Introduction to Dependent Types

Just what are "dependent types"? Furthermore: What is a dependently typed programming language?

This talk is going to provide answers to these questions by beginning with the the programming language theoretic basis to the notion of dependent types as a simple extension to the simply typed λ-calculus (STLC), and ending with how we might implement a typechecker and interpreter for a such a calculus (notably, λΠ).

Prior knowledge of the STLC, capture avoiding substitution, the basics of modern PL theory notation, and the set of GHC extensions encompassed in the notion of "Dependent Haskell" is encouraged (but not required) to fully enjoy the content of this talk.

The presentation will aim to be 30 minutes in length with plenty of time for questions and discussion afterwards.

---

The building is right across the street from the Sunnyvale Caltrain station. The Target office is located on the second floor.

We will have someone in the lobby to let you in until about 7:00. After, 7:00 please leave a comment here or text 650-741-8406 and we can send someone to let you in.

Please note that there is free 3hr street and garage available parking near the building. However, you can NOT park where there are gates and/or ticket machines controlling access to the garages.