A Multiparty Multi-Session Logic

Recent work on the enhancement of multiparty sessions types with logical annotations enables not only the validation of structural properties of the conversations and on the sorts of the messages, but also the validation of properties on the actual values exchanged. However, the specification and verification of the mutual effects of multiple cross-session interactions is still an open problem. We introduce a multiparty logical proof system with virtual states that enables the tractable specification and validation of fine-grained inter-session correctness properties of processes participating in several interleaved sessions. We present a sound and relatively complete static verification method.