Semantics of an Effect Analysis for Exceptions
- Nick Benton ,
- Peter Buchlovsky
Proceedings of the Third ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI '07) |
Published by ACM
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.