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

Official URL: https://doi.org/10.3233/FI-2010-304

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.

ORCID iDs

Löh, Andres, Mcbride, Conor

and Swierstra, Wouter;

Citations and altmetrics

Item metadata

Item type:	Article
ID code:	36006
Dates:	Date Event 2010 Published 24 September 2010 Published Online
Keywords:	core calculus, lambda calculus, Haskell, Electronic computers. Computer science, Computational Theory and Mathematics, Algebra and Number Theory, Theoretical Computer Science, Information Systems
Subjects:	Science > Mathematics > Electronic computers. Computer science
Department:	Faculty of Science > Computer and Information Sciences
Depositing user:	Pure Administrator
Date deposited:	18 Nov 2011 05:21
Last modified:	20 Jan 2021 19:42
Related URLs:	Scopus publication
URI:	https://strathprints.strath.ac.uk/id/eprint/36006

Export

CORE (COnnecting REpositories)