Session types statically guarantee that communication complies with a protocol. However, most accounts of
session typing do not account for failure, which means they are of limited use in real applicationsÐespecially
distributed applicationsÐwhere failure is pervasive.
We present the first formal integration of asynchronous session types with exception handling in a functional
programming language. We define a core calculus which satisfies preservation and progress properties, is
deadlock free, confluent, and terminating.
We provide the first implementation of session types with exception handling for a fully-fledged functional
programming language, by extending the Links web programming language; our implementation draws
on existing work on effect handlers. We illustrate our approach through a running example of two-factor
authentication, and a larger example of a session-based chat application where communication occurs over
session-typed channels and disconnections are handled gracefully.
The University of Kansas prohibits discrimination on the basis of race, color, ethnicity, religion, sex, national origin, age, ancestry, disability, status as a veteran, sexual orientation, marital status, parental status, gender identity, gender expression and genetic information in the University’s programs and activities. The following person has been designated to handle inquiries regarding the non-discrimination policies: Director of the Office of Institutional Opportunity and Access, IOA@ku.edu, 1246 W. Campus Road, Room 153A, Lawrence, KS, 66045, (785)864-6414, 711 TTY.