A Tutorial Implementation of a Dependently Typed Lambda Calculus

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.

Andres Löh, 2009-09-23