π計算を介したプログラム検証・解析

• Project/Area Number: 24K20731
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: The University of Tokyo
• Principal Investigator: 酒寄 健 東京大学, 大学院情報理工学系研究科, 助教 (80990803)
• Project Period (FY): 2024-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000); Fiscal Year 2027: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2025: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2024: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
• Keywords: プログラミング言語 / π計算

Outline of Research at the Start

本研究はπ 計算という計算体系を使用することで、各言語から独立した汎用的なプログラミング言語の理論的研究基盤の樹立を目指す。例えるならば、コンパイラ基盤であるLLVM が多用なプログラミング言語のコンパイル先として利用され、そこで言語に依存しない最適化がなされているように、π 計算を多用な(理論的な) プログラミング言語の翻訳先として利用する。そして、π 計算に対する解析を行うことで、元のプログラムの(1）プログラム等価性の検証および(2）実行時間などのコストの解析・検証をすることを目指す。