Specifying Byrd's Box Model with a Continuation Semantics

AbstractWe give a formal specification of Byrd's box model. This specification is based on a on a Prolog operational semantics with continuations. We also show how this specification can be executed by a direct translation into λProlog, leading to a Prolog interpreter that produces execution traces. This interpreter can be used both to experiment various trace models to validate them. We have hence a formal framework to specify and prototype trace models