By Thorsten Altenkirch and Bernhard Reus, from CSL 1999, available from Thorsten Altenkirch’s website:
We present a definition of untyped lambda-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended a Kleisli triple, which is a concise way to verify the substitution laws for lambda-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 lambda-calculus using dependent types, and show that this is an instance of a generalisation of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.