A tutorial implementation of a dependently typed lambda calculus

Andres Löh, Conor Mcbride, Wouter Swierstra

Research output: Contribution to journalArticlepeer-review

18 Citations (Scopus)


We present the type rules for a dependently typed core calculus together with a straight-forward 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 article is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe.
Original languageEnglish
Pages (from-to)177-207
Number of pages31
JournalFundamenta Informaticae
Issue number2
Early online date24 Sept 2010
Publication statusPublished - 2010


  • core calculus
  • lambda calculus
  • Haskell


Dive into the research topics of 'A tutorial implementation of a dependently typed lambda calculus'. Together they form a unique fingerprint.

Cite this