We present a definition of untyped A-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 A-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 A-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.
CITATION STYLE
Altenkirch, T., & Reus, B. (1999). Monadic presentations of lambda terms using generalized inductive types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1683, pp. 453–468). Springer Verlag. https://doi.org/10.1007/3-540-48168-0_32
Mendeley helps you to discover research relevant for your work.