No.050 Software Contracts for Communication, Monitoring, and Security

Session types describe the sequence and format of messages on point-to-point communication channels. They allow communication protocols to be specified type-theoretically so that their implementations can be verified by static type-checking. Session types were introduced in the setting of process calculus, and later formulated for imperative, functional and object-oriented languages. The quest for a clean integration of session types and objects leads to the idea of embedding session types in a more general setting of typestate, in which the operations available for a given object are state-dependent. We are exploring this idea with a typestate system in which typestate specifications are inspired by session types, and developing an experimental implementation as an extension of Java.

Joint work with Vasco Vasconcelos, Antonio Ravara, Nils Gesbert, Ornela Dardha, Dimitrios Kouzapas