Implementing ADependently Typed Lambda Calculus
Stc
Date: 2007-04-12
Time: 11:45
Room: BBL room 471
Speaker: Wouter Swierstra (University of Nottingham)
Title: Implementing a Dependently Typed Lambda Calculus
Abstract
Most Haskell programmers know how to implement a type checker for the
simply typed lambda calculus. Quite a few know how to implement
Hindley-Milner style type inference. When it comes to implementing a
dependently typed calculus, however, most people don't even know
where to start. Based on experience with Epigram, I hope to show how
to implement the most rudimentary core of a dependently typed
programming language. Surprisingly, the implementation is no more
difficult than that for the simply typed lambda calculus.
Note: I'll not assume any prior knowledge about dependent types,
though it might help if you have some experience with turning
inference rules into Haskell code. This is joint work with Conor
McBride and Andres Loeh.
