Many theoretical results about programming languages are stated for
effect-free lambda calculus only, or add effects (such as I/O and state) in
an ad-hoc manner. With his computational monads, Moggi presented an
abstract framework that fits a wide range of computational effects. Some
languages, notably ob ject-oriented ones, feature subtyping in addition to
effects.
In my Bachelor thesis I present an extension of Moggi’s computational
monads with subtyping. As an application of the theory we show that
Abadi and Cardelli’s imperative ob ject calculus can be embedded into
our system, in a way that ensures type safety.