Tuesday, December 3, 2019 - 12:30pm
Location:4513 Newell-Simon Hall
Speaker:CHUTA SANO, Masters Student https://www.linkedin.com/in/chutasano
On Session Typed Contracts for Imperative Languages
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 ordinary type systems, have been extended to monitors, which are 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.