Marco Maggesi (joint work with Andre' Hirschowitz)
[2008-09-05] An new version of the Coq formalization of the theorem is available.
[2006-09-07] An other formalization of the theorem in HOL-Light is available.
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.