Session types are used to describe the structure of communications across channels. Previous research has established a message-passing interpretation of intuitionistic linear logic. Meanwhile, communication failures have been an important research topic in session types. However, the exception handling mechanism has not been well studied in the context of message passing. To bridge this gap, we study the interpretation of classical affine logic and propose a new type system containing features such as explicit channel cancellation and exception handling constructors. Our type system ensures program safety by enforcing session fidelity and deadlock freedom. To experiment, we implemented an interpreter for our language and tested it on several examples to match the expected process behavior. Additionally, we explore the possibility of representing some programming features, such as uncaught exceptions and non-exhaustive matches, by revisiting the system.

61 pages

Advisor
Frank Pfenning

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu