A Tutorial Implementation of a Dependently Typed Lambda Calculus

Issue title: Dependently Typed Programming

Article type: Research Article

Authors: Löh, Andres | McBride, Conor | Swierstra, Wouter

Affiliations: Utrecht University, The Netherlands. andres@cs.uu.nl | University of Strathclyde, U.K. conor.mcbride@cis.strath.ac.uk | Vector Fabrics, The Netherlands. wouter@vectorfabrics.com

Note: [] Address for correspondence: Dept. of Information and Computing Sciences, Universiteit Utrecht, P.O. Box 80.089, NL-3508, TB Utrecht, The Netherlands

Abstract: 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.

DOI: 10.3233/FI-2010-304

Journal: Fundamenta Informaticae, vol. 102, no. 2, pp. 177-207, 2010