Proving Exception Stackability and Linearity in an Ordered Logical Framework

We formally prove the stackability and linearity of exception handlers of ML-style semantics using a novel proof technique via an ordered logical framework (OLF). We first transform exceptions into continuation-passing-style (CPS) terms and formalize the exception properties as a judgement on the CPS terms. Then, rather than directly proving that the properties hold for terms, we prove our theorem for the representations of the CPS terms and transform in OLF. We rely upon the correctness of our representations to transfer the results back to the actual CPS terms and transform. Our work can be seen as two-fold: we present a theoretical justification of using the stack mechanism to implement exceptions of ML-like semantics; and we demonstrate the value of an ordered logical framework as a conceptual tool in the theoretical study of programming languages.