Session-typed programming in unreliable communication environment
| Project/Area Number |
17K12662
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Gifu University |
|---|
Principal Investigator |
Imai Keigo 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| Project Period (FY) |
2017-04-01 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2020: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 並行システム / 通信プロトコル / セッション型 / 関数型プログラミング / ドメイン特化言語 / 並行計算 / OCaml / 型システム / メタプログラミング / ステージ計算 / モナド / 線形型 / 構文拡張 / デッドロック / 型理論 / プロトコル |
|---|
| Outline of Final Research Achievements |
The main results of this research are: (1) Programming frameworks for session types for two-party communication, which has been realised in OCaml and C#. (2) Programming frameworks for multiparty session types that handle communication between three or more parties. The results are accepted at higher-tier venues including ECOOP 2020, FLOPS 2020 and TACAS 2022. Furthermore, one of the results in multiparty session types is extended to the mixed choice, which is an abstract model for timeout in an communication. By establishing mixed choice and timeout in multiparty session types, we opened the design space for session types in the unreliable communication environment.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究の主要な学術的意義は，セッション型の多彩な実現手法とその特徴を明らかにしたことと，その具体的な実装を与えたことである．セッション型は，既存のプログラミング言語の型とは大きなギャップが存在した．本研究により，そのままでは信頼性高く構築することが困難な並行・分散プログラムを，プログラミング言語の主要な信頼性保証技法である「型」の枠組みで，安全に効率よく開発できることが期待される．さらに，本研究が最終的に実現したmixed choiceの枠組みを発展させることで，メッセージの到達性を保証しない環境における通信プログラミング手法の確立が強く期待できる．
|
Report
(6 results)
Research Products
(38 results)
