Message-passing provides a powerful method for communication in concurrent programs, where processes communicate by sending messages over channels. Session types statically guarantee that communication over a channel adheres to a specified protocol. However, standard session types assume that channels remain active until protocol completion—an unrealistic assumption, because processes often might fail due to exceptions.

We present an integration of session types with explicit exceptions that makes communication failures a concern tracked at the type level. Unlike standard session types, our protocols do not only keep track of the type of messages that are exchanged, but also whether either side of the channel might be canceled, and with which corresponding exception type. Our approach provides two models: (1) a synchronous model by translation to standard session types, and (2) a native asynchronous model where send operations are both non-blocking and fail for canceled channels. Both models support controlled channel termination from either side of the channel with exception values.

We show that the asynchronous model is sound by verifying end-to-end correctness with respect to a low-level lock-free channel implementation with a cancel operation. We also show that both our systems can be extended to dependent protocols in the style of the Actris framework. This verification is fully mechanized in the Iris separation logic framework using the Rocq proof assistant.

This is joint work with Léon Ducruet, Anton Lorenzen, and Robbert Krebbers.