| Project/Area Number |
20K11743
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Institute of Science Tokyo |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Completed (Fiscal Year 2024)
|
| Budget Amount *help |
¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000)
Fiscal Year 2023: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2021: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2020: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 関数型言語 / 例外処理 / 継続 / 制御捕獲 / 型システム / ラムダ計算 / 関数プログラミング / プログラミング言語理論 / call/cc / プログラム理論 / プログラミング言語 / 大域脱出 / 関数型プログラミング言語 / dynamic-wind / 制御捕捉 / 一級継続 / 一級環境 / 制御構造 |
|---|
| Outline of Research at the Start |
制御捕獲）は制御の流れを強制的に捕獲するしくみであり，Javaのfinallyブロック，Schemeのdynamic-windが代表的である。 そして，例外処理機構は，大域脱出 と制御捕獲により構成されている。この制御捕獲については理論的側面において未解明である。 本研究では，これまでの大域脱出・一級継続の研究結果を基盤として，制御捕獲の計算モデ ルを提案する。関数型言語の計算モデルであるラムダ計算を始めとして，様々なプログラミングパラダイムに対しても研究を進める。さらにその計算モデルを基盤として，制御捕獲機能を有する例外処理機構に対するソフトウェア検証手法と確立する。
|
| Outline of Final Research Achievements |
This study focused on control capturing in exception handling, such as finally and dynamic-wind, which have not been studied much in theory. Based on earlier research on non-local exits and first-class continuations, we made a new computational model using lambda calculus and effect systems. We studied this model with formal methods from mathematical logic, especially linear logic and sequent calculus, and explained how control capture works in theory. We also applied our model to various programming styles, like functional, imperative, object-oriented, and distributed languages. As a result, our research gives a base for checking and analyzing programs that use these kinds of exception-handling features.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究は、従来理論的検討が不足していたコントロールキャプチャ機能に注目し、計算モデルを構築し数理論理学的に定式化した点に学術的意義がある。継続、例外処理、動的スコープなどに対し、線形論理やシーケント計算を用いた理論的枠組みは、ラムダ計算や型理論の新たな発展に貢献する。さらに、例外処理機構が果たす役割を形式的に分析することで、安全性や堅牢性が求められるソフトウェアの信頼性向上に寄与する。特に入出力終了処理のような側面を検証可能にする意義は大きく、実用的な開発への応用も期待される。また、複数の言語パラダイムに対応する理論を提供することで、今後の高信頼ソフトウェア開発の基盤技術となる可能性を持つ。
|
