| Item type |
Trans(1) |
| 公開日 |
2022-07-04 |
| タイトル |
|
|
タイトル |
Verifying Session-Typed Concurrent Programs Using Typed PPX in OCaml |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Verifying Session-Typed Concurrent Programs Using Typed PPX in OCaml |
| 言語 |
|
|
言語 |
eng |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[発表概要, Unrefereed Presentatin Abstract] |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
Gifu University |
| 著者所属 |
|
|
|
Royal Holloway, University of London |
| 著者所属 |
|
|
|
Brunel University London |
| 著者所属(英) |
|
|
|
en |
|
|
Gifu University |
| 著者所属(英) |
|
|
|
en |
|
|
Royal Holloway, University of London |
| 著者所属(英) |
|
|
|
en |
|
|
Brunel University London |
| 著者名 |
Keigo, Imai
Julien, Lange
Rumyana, Neykova
|
| 著者名(英) |
Keigo, Imai
Julien, Lange
Rumyana, Neykova
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
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. |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
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. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA11464814 |
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO）
巻 15,
号 3,
p. 2-2,
発行日 2022-07-04
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7802 |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-TPRO1503004.pdf (26.9 kB)
