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 (https://doi.org/10.3233/FI-2010-304)
Full text not available in this repository.Request a copyAbstract
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 ORCID: https://orcid.org/0000-0003-1487-0886 and Swierstra, Wouter;-
-
Item type: Article ID code: 36006 Dates: DateEvent2010Published24 September 2010Published OnlineSubjects: 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: 31 Aug 2024 05:39 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/36006