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
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.
Download PDF Show BibTeX
Login to edit