Sciweavers

FUIN
2010

A Tutorial Implementation of a Dependently Typed Lambda Calculus

13 years 8 months ago
A Tutorial Implementation of a Dependently Typed Lambda Calculus
Abstract. 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 article is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe.
Andres Löh, Conor McBride, Wouter Swierstra
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where FUIN
Authors Andres Löh, Conor McBride, Wouter Swierstra
Comments (0)