Modelling of Control Capture and Its Applications

2024 Fiscal Year Final Research Report

• 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: Nishizaki Shin-ya 東京科学大学, 情報基盤センター, 教授 (90263615)
• Project Period (FY): 2020-04-01 – 2025-03-31
• Keywords: 関数型言語 / 例外処理 / 継続 / 制御捕獲

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.

Free Research Field

プログラミング言語理論

Academic Significance and Societal Importance of the Research Achievements

本研究は、従来理論的検討が不足していたコントロールキャプチャ機能に注目し、計算モデルを構築し数理論理学的に定式化した点に学術的意義がある。継続、例外処理、動的スコープなどに対し、線形論理やシーケント計算を用いた理論的枠組みは、ラムダ計算や型理論の新たな発展に貢献する。さらに、例外処理機構が果たす役割を形式的に分析することで、安全性や堅牢性が求められるソフトウェアの信頼性向上に寄与する。特に入出力終了処理のような側面を検証可能にする意義は大きく、実用的な開発への応用も期待される。また、複数の言語パラダイムに対応する理論を提供することで、今後の高信頼ソフトウェア開発の基盤技術となる可能性を持つ。