Brunel University Research Archive(BURA) preserves and enables easy and open access to all
types of digital content. It showcases Brunel's research outputs.
Research contained within BURA is open access, although some publications may be subject
to publisher imposed embargoes. All awarded PhD theses are also archived on BURA.
Please use this identifier to cite or link to this item:
http://bura.brunel.ac.uk/handle/2438/26564| Title: | Kmclib: Automated Inference and Verification of Session Types from OCaml Programs |
| Authors: | Imai, K Lange, J Neykova, R |
| Keywords: | multiparty session types;concurrent programming;OCaml |
| Issue Date: | 30-Mar-2022 |
| Publisher: | Springer, Cham |
| Citation: | Imai, K., Lange, J. and Neykova, R. (2022) 'Kmclib: Automated Inference and Verification of Session Types from OCaml Programs', in Fisman, D. and Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2022. (Lecture Notes in Computer Science, vol 13243). Cham, Switzerland: Springer, Cham, pp. 379 - 386. doi: 10.1007/978-3-030-99524-9_20. |
| Abstract: | Copyright © 2022 The Author(s). Theories 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 [15]). Well-typed programs, written with kmclib, do not lead to communication errors and cannot get stuck. |
| URI: | https://bura.brunel.ac.uk/handle/2438/26564 |
| DOI: | https://doi.org/10.1007/978-3-030-99524-9_20 |
| ISBN: | 978-3-030-99523-2 (hbk) 978-3-030-99524-9 (ebk) |
| Other Identifiers: | ORCID iD: Keigo Imai https://orcid.org/0000-0003-1602-8473; Julien Lange https://orcid.org/0000-0001-9697-1378; Rumyana Neykova https://orcid.org/0000-0002-2755-7728. 20 |
| Appears in Collections: | Dept of Computer Science Research Papers |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| FullText.pdf | Copyright © 2022 The Author(s). Rights and permissions: Open Access. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. | 19.99 MB | Adobe PDF | View/Open |
This item is licensed under a Creative Commons License
