| dc.description.abstract | This thesis investigates both theory and applications of the monad in a functional setting. Monads are constructs simulating different types of computations, such as indeterminism, exception handling, stateful computations, IO, and much more, all in the functional paradigm. The thesis starts by defining the monad, and builds up the theory around it. Three large implementaional examples using monads are presented: One implementation of a small interpreter for lambda calculus with graph sharing, one framework for writing symmetric cryptographic algorithms, and one more theoretical construction of a catamorphism and comprehension based monadic query language. All of these examples uses combinations of several monads to form complex computations with a high level of expressiveness. Other related constructs are discussed, as well as a presentation of the foundation for monads in category theory. A new monad is also introduced, the Pair monad. This monad is a generalisation of the list monad, and simulates substitution in tree-like structures, such as lambda terms. Furthermore, the thesis makes an investigation into the Curry-Howard Correspondence with a first order lambda calculus extended with monads, called computational lambda calculus. This results in a sublogic of constructive S4 modal logic. The thesis also uses the Kripke semantic for this logic to deduce a Kripke semantic for type setting lambda terms in computational lambda calculus. | eng |