On Session Typed Contracts for Imperative Languages
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 2019
- Accession Number
- AD1120838
Entities
People
- Chuta Sano
Organizations
- Carnegie Mellon University