A Tutorial Implementation of a Dependently Typed Lambda Calculus
Andres Löh, Conor McBride and Wouter Swierstra

We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe.

Download
Paper (published in FI, revised summer 2009)
Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources)
prelude.lp (prelude for the LambdaPi interpreter, containing several example programs)
Instructions (how to get started with the LambdaPi interpreter)
Old draft (original FI submission)
Old draft
Even older draft (called "Simply Easy")
Links
Agda 2, a dependently typed programming language being developed at Chalmers.
Epigram, a dependently typed programming language being developed at Nottingham.
Coq, a proof assistant being developed at INRIA.
Cayenne, a dependently typed programming language by Lennart Augustsson.

Valid XHTML 1.0! Valid CSS! Get Firefox!

Andres Löh, 2009-09-23