Modules over monads and lambda-calculi
- Marco Maggesi
- André Hirschowitz
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).
module, monad, category, lambda calculus, higher order syntax
Modules over monads and lambda-calculi ====================================== Content of the distribution: Misc.v : Miscellanea Quot.v : Axiomatic definition of quotient types. Extensionality.v : Axiom of extensionality. Monad.v, Mod.v : Theory of monads and modules over a monad. Slc.v, Lc.v : Theory of Simple Lambda Calculus (syntax, semantic). Derived_Mod.v : Derived modules. Lc_exp.v : The main theorem.