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)

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

Mcbride, Conor ORCID: https://orcid.org/0000-0003-1487-0886

• Share and Export
  

  ReferAtomJSONOpenURL ContextObject in SpanMPEG-21 DIDLRDF+XMLRDF+N-TriplesRefWorksHTML CitationEndNoteMultiline CSVRIS (EndNote Online, Zotero, Ref manager, etc)Data Cite XMLDublin CoreEP3 XMLASCII CitationRDF+N3METSSimple MetadataRIOXX2 XMLBibTeXOpenURL ContextObjectMODS
• Item metadata

  Item type:	Article
  ID code:	36006
  Dates:	Date Event 2010 Published 24 September 2010 Published Online
  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:	11 Nov 2024 09:54
  Related URLs:	Scopus publication
  URI:	https://strathprints.strath.ac.uk/id/eprint/36006