Contribution: lc

Modules over monads and lambda-calculi

Authors

Description

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).

Keywords

module, monad, category, lambda calculus, higher order syntax

README

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.

Available files