Formalization of Lambda Calculus in Coq HOL and

We define a notion of module over a monad and use it to propose a new definition (or semantics) for abstract syntax (with binding constructions). Using our notion of module, we build a category of exponential monads, which can be understood as the category of lambda-calculi, and prove that it has an initial object (the pure untyped lambda-calculus). Our definitions and results are formalized in the proof assistant Coq. Abstract. We define a notion of module over it to propose a new definition (or semantics) for (with binding constructions). Using our notion of a category of exponential monads, which can be category of lambda-calculi, and prove that it has (the pure untyped lambda-calculus). Our definitions are formalized in the proof assistant Coq.