Correspondence Assertions for Process Synchronization in Concurrent Communications

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types [Honda, K., V. Vasconcelos and M. Kubo, Language primitives and type discipline for structured communication-based programming, in: Proc. of ESOP'98, LNCS (1998), pp. 122–138]. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions [Clarke, E. and W. Marrero, Using formal methods for analyzing security, Information Survivability Workshop (1998), Gordon, A. and A. Jeffrey, Typing correspondence assertions for communication protocols, in: Seventeenth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2001), number 45 in ENTCS (2001)]. The resulting type discipline augments the types of long term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address the shortcomings present in the pure theory of session types. Keywords: Concurrent programming, pi-calculus, type systems, session types, correspondence assertions