Computer Science Masters Thesis Presentation

  • CHUTA SANO
  • Masters Student
  • Computer Science Department
  • Carnegie Mellon University
Master's Thesis Presentation

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.

Thesis Committee:
Frank Pfenning
Iliano Cervesato

Additional Thesis Information

For More Information, Please Contact: 
Keywords: