Picture of two heads

Open Access research that challenges the mind...

The Strathprints institutional repository is a digital archive of University of Strathclyde research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including those from the School of Psychological Sciences & Health - but also papers by researchers based within the Faculties of Science, Engineering, Humanities & Social Sciences, and from the Strathclyde Business School.

Discover more...

A tutorial implementation of a dependently typed lambda calculus

Löh, Andres and Mcbride, Conor and Swierstra, Wouter (2010) A tutorial implementation of a dependently typed lambda calculus. Fundamenta Informaticae, 102 (2). pp. 177-207. ISSN 0169-2968

Full text not available in this repository. (Request a copy from the Strathclyde author)

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.