The Logic of Fault-Tolerance in Message-Passing Concurrency
Bas van den Heuvel

Abstract:
Exception handling is a widespread method of making programs fault-tolerant. Exploiting a Curry-Howard correspondence with linear logic, Caires and Pérez have shown how to use modalities denoting non-deterministically available behaviour in the π-calculus to interpret a functional programming language with exception handling. Their work did, however, not address constructs for exception handling in the relevant setting of programming languages with message-passing concurrency. This thesis focusses on this limitation, and uses their ideas to give a new, logically motivated account of exception handling in message-passing concurrency. As key reference in this study, we examine the typed framework for interactional exception handling by Carbone et al., which is fairly expressive, but does not rest upon Curry-Howard foundations. We identify a fragment of this framework on which we can define a conversion to an asynchronous version of the typed π-calculus from Caires and Pérez. Our main result is that source processes and their respective conversions correspond in terms of typing and progress; based on our conversion, we conjecture an operational correspondence result.