On Session Typed Contracts for Imperative Languages
[Technical Report, Master's Thesis]
Carnegie Mellon University
Pagination or Media Count:
Session types prescribe the protocols for communication between concurrently executing processes. Following discoveries of the correspondence between intuitionistic linear logic and linear session types, there have been many related works ranging from practical implementations to theoretical extensions. In particular, linear session types, which assume a strong condition that there is only one client for a session, have been extended to shared session types, which introduce semantics for multiple clients. This extension was subsequently implemented in an imperative setting in the language Concurrent C0. In another direction, contracts, which are well-studied constructs in languages without session types, have been extended to monitors, or contracts for linear session types, in the usual functional setting. In this work, we formalize an imperative programming language based on previous work which implements both linear and shared session typed channels and adapt the monitors to the imperative setting. We further extend the notion of monitoring to shared session types and introduce its semantics. Finally, we introduce several case studies of linear and shared monitors.
- Theoretical Mathematics
- Numerical Mathematics
- Computer Programming and Software