@article{oai:ipsj.ixsq.nii.ac.jp:00218756,
 author = {Keigo, Imai and Julien, Lange and Rumyana, Neykova and Keigo, Imai and Julien, Lange and Rumyana, Neykova},
 issue = {3},
 journal = {情報処理学会論文誌プログラミング（PRO）},
 month = {Jul},
 note = {This presentation introduces the design and implementation of kmclib: an OCaml library that supports the development of correct message-passing programs. The development workflow in kmclib utilises type inference and PreProcessor eXtension (PPX) in OCaml. The kmclib primitives allow the vanilla OCaml typechecker to infer the communication structure of a program. The preprocessor for kmclib is typed: it exploits OCaml's compilerlib to extract session types and verify their compatibility (k-MC). Well-typed programs, written with kmclib, do not lead to communication errors and cannot get stuck., This presentation introduces the design and implementation of kmclib: an OCaml library that supports the development of correct message-passing programs. The development workflow in kmclib utilises type inference and PreProcessor eXtension (PPX) in OCaml. The kmclib primitives allow the vanilla OCaml typechecker to infer the communication structure of a program. The preprocessor for kmclib is typed: it exploits OCaml's compilerlib to extract session types and verify their compatibility (k-MC). Well-typed programs, written with kmclib, do not lead to communication errors and cannot get stuck.},
 pages = {2--2},
 title = {Verifying Session-Typed Concurrent Programs Using Typed PPX in OCaml},
 volume = {15},
 year = {2022}
}