Projects per year
Combining local exceptions and first class continuations leads to programs with complex control flow, as well as the possibility of expressing powerful constructs such as resumable exceptions. We describe and compare games models for a programming language which includes these features, as well as higher-order references. They are obtained by contrasting methodologies: by annotating sequences of moves with "control pointers" indicating where exceptions are thrown and caught, and by composing the exceptions and continuations monads. The former approach allows an explicit representation of control flow in games for exceptions, and hence a straightforward proof of definability (full abstraction) by factorization, as well as offering the possibility of a semantic approach to control flow analysis of exception-handling. However, establishing soundness of such a concrete and complex model is a non-trivial problem. It may be resolved by establishing a correspondence with the monad semantics, based on erasing explicit exception moves and replacing them with control pointers.
|Publication status||Published - 5 Sept 2013|
- F.3.2, F.3.3
FingerprintDive into the research topics of 'Combining and relating control effects and their semantics'. Together they form a unique fingerprint.
- 1 Finished
Semantic Structures for Higher-Order Information Flow
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council