Polymorphic Subtyping for Effect Analysis: the Algroithm

Abstract

We study an annotated type and effect system that integrates let-polymorphism, effects, and sybtyping into an annotated type and effect system for a fragment of Concurrent ML. First a type inference algorithm and a procedure for constraint normalisation and simplification are defined, and next they are proved syntactically sound with respect to the annotated type and effect system.