Semantics of an Effect Analysis for Exceptions
Nick Benton and Peter Buchlovsky
The ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2007)
Nice, France, January 16, 2007
Abstract
We give a semantics to a polymorphic effect analysis that tracks possibly-thrown exceptions and possible non-termination for a higher order language. The semantics is defined using partial equivalence relations over a standard monadic, domain-theoretic model of the original language and establishes the correctness of both the analysis itself and of the contextual program transformations that it enables.