Monadic Presentations of Lambda Terms Using Generalized Inductive Types

Altenkirch, Thorsten and Reus, Bernhard (1999) Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In: Flum, Jörg and Rodriguez-Artalejo, Mario (eds.) Computer Science Logic: Proceedings of the 13th International Workshop CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain. Lecture Notes in Computer Science, 1863 . Springer-Verlag, pp. 453-468. ISBN 9783540665366

[img] Postscript
Restricted to SRO admin only

Download (415kB)

Abstract

We present a definition of untyped l-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended to a Kleisli triple, which is a concise way to verify the substitution laws for l-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed l-calculus using dependent types, and show that this is an instance of a generalization of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.

Item Type: Book Section
Keywords: Type Theory, inductive types, l-calculus, category theory.
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Chris Keene
Date Deposited: 03 Mar 2008
Last Modified: 30 Nov 2012 16:51
URI: http://sro.sussex.ac.uk/id/eprint/1435
Google Scholar:101 Citations

View download statistics for this item

📧 Request an update