Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
Kmclib: Automated Inference and Verification of Session Types from OCaml Programs
复制标题
Kmclib：从 OCaml 程序自动推断和验证会话类型
DOI：
10.1007/978-3-030-99524-9_20
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Rumyana Neykova
中科院分区：
文献类型：
--
作者：
Keigo Imai;Julien Lange;Rumyana Neykova
基于多方会话类型的理论和工具为使用消息传递进行通信的并发程序提供了正确性保证。这些保证通常是以自上而下的方法为代价的，这种方法要求整个程序的通信行为被指定为一个全局类型。本文介绍了kmclib：一个OCaml库，它支持开发正确的消息传递程序，而不必编写任何类型。该库利用OCaml的元编程工具来自动推断并发程序的会话类型并验证其兼容性（k-MC）。用kmclib编写的类型良好的程序不会导致通信错误，也不会卡住。
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 introduceskmclib: an OCaml library that supports the development ofcorrectmessage-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 withkmclib, do not lead to communication errors and cannot get stuck.