Skip to main content
Kent Academic Repository

Embedding Session Types in HML

Bocchi, Laura, Demangeon, Romain (2013) Embedding Session Types in HML. In: Electronic Proceedings in Theoretical Computer Science. 137 (1). pp. 53-62. (doi:10.4204/EPTCS.137.5) (KAR id:43739)


Recent work on the enhancement of multiparty session types with logical annotations enable the effective verification of properties on (1) the structure of the conversations, (2) the sorts of the messages, and (3) the actual values exchanged. In [3] we extend this work to enable the specification and verification of mutual effects of multiple cross-session interactions. Here we give a sound and complete embedding into the Hennessy-Milner logic to justify the expressiveness of the approach in [3] and to provide it with a logical background that will enable us to compare it with similar approaches.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.4204/EPTCS.137.5
Subjects: Q Science > QA Mathematics (inc Computing science) > QA299 Analysis, Calculus
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Laura Bocchi
Date Deposited: 05 Nov 2014 10:12 UTC
Last Modified: 10 Dec 2022 23:10 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.