Monadic Presentations of Lambda Terms Using Generalized Inductive Types Export

@incollection{citeulike:6074784, abstract = {We present a definition of untyped λ-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 λ-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 λ-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.}, author = {Altenkirch, Thorsten and Reus, Bernhard}, citeulike-article-id = {6074784}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-48168-0_32}, citeulike-linkout-1 = {http://www.springerlink.com/content/egmaxxm18wfuhd5c}, doi = {10.1007/3-540-48168-0_32}, journal = {Computer Science Logic}, keywords = {kleisli-structures, monads, types}, pages = {825}, posted-at = {2009-11-05 15:47:57}, priority = {2}, title = {Monadic Presentations of Lambda Terms Using Generalized Inductive Types}, url = {http://dx.doi.org/10.1007/3-540-48168-0_32}, year = {2009} }

TY - CHAP ID - citeulike:6074784 L3 - citeulike-article-id:6074784 N2 - We present a definition of untyped λ-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 λ-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 λ-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. JF - Computer Science Logic EP - 825 TI - Monadic Presentations of Lambda Terms Using Generalized Inductive Types SP - 825 KW - kleisli-structures KW - monads KW - types AU - Altenkirch, Thorsten AU - Reus, Bernhard PY - 2009/// UR - http://dx.doi.org/10.1007/3-540-48168-0_32 ER -