Coherence of subsumption for monadic types

Abstract

Abstract One approach to give semantics to languages with subtypes is by translation to target languages without subtyping: subtypings A ≤ B are interpreted via conversion functions A → B . This paper shows how to extend the method to languages with computational effects, using Moggi's computational metalanguage.