1. Brunel University Research Archive
  2. College of Engineering, Design and Physical Sciences
  3. Dept of Computer Science
  4. Dept of Computer Science Research Papers
Please use this identifier to cite or link to this item: http://bura.brunel.ac.uk/handle/2438/26560
Full metadata record
DC FieldValueLanguage
dc.contributor.authorImai, K-
dc.contributor.authorLange, J-
dc.contributor.authorNeykova, R-
dc.date.accessioned2023-05-28T16:18:54Z-
dc.date.available2023-05-28T16:18:54Z-
dc.date.issued2019-11-26-
dc.identifierhttps://arxiv.org/abs/2111.12147v2-
dc.identifierORCID iD: Rumyana Neykova https://orcid.org/0000-0002-2755-7728-
dc.identifier.citationImai, K., Lange, J. and Neykova, R. (2019) 'kmclib: Automated Inference and Verification of Session Types', Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, arXiv:2111.12147v2 [cs.PL], pp. 1 - 11. doi: 10.48550/arXiv.2111.12147.en_US
dc.identifier.issn2331-8422-
dc.identifier.urihttps://bura.brunel.ac.uk/handle/2438/26560-
dc.descriptionarXiv preprint. A version of this paper was published under a Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/) by Springer, Cham, 30 March 2022, at: https://doi.org/10.1007/978-3-030-99524-9_20.en_US
dc.description.abstractTheories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrinsically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type. This paper introduces kmclib: an OCaml library that supports the development of correct message-passing programs without having to write any types. The library utilises the meta-programming facilities of OCaml to automatically infer the session types of concurrent programs and verify their compatibility (k-MC). Well-typed programs, written with kmclib, do not lead to communication errors and cannot get stucken_US
dc.description.sponsorship...en_US
dc.format.extent1 - 11-
dc.language.isoen_USen_US
dc.publisherCornell Universityen_US
dc.relation.urihttps://doi.org/10.1007/978-3-030-99524-9_20-
dc.rightsMade available on arXiv under a CC BY: Creative Commons Attribution This license allows reusers to distribute, remix, adapt, and build upon the material in any medium or format, so long as attribution is given to the creator. The license allows for commercial use.-
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/-
dc.subjectmultiparty session typesen_US
dc.subjectconcurrent programmingen_US
dc.subjectOCamlen_US
dc.titlekmclib: Automated Inference and Verification of Session Typesen_US
dc.typeArticleen_US
dc.identifier.doihttps://doi.org/10.48550/arXiv.2111.12147-
dc.relation.isPartOfTools and Algorithms for the Construction and Analysis of Systems - 27th International Conference-
pubs.publication-statusPreprint published online-
dc.rights.holderThe Authors-
Appears in Collections:Dept of Computer Science Research Papers

Files in This Item:
File Description SizeFormat 
Preprint.pdfMade available on arXiv under a CC BY: Creative Commons Attribution This license allows reusers to distribute, remix, adapt, and build upon the material in any medium or format, so long as attribution is given to the creator. The license allows for commercial use.723.51 kBAdobe PDFView/Open
Show simple item record


This item is licensed under a Creative Commons License Creative Commons