Universal models of programming languages and program reasoning

2021 Fiscal Year Final Research Report

• Project/Area Number: 18K11156
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Tohoku University
• Principal Investigator: Asada Kazuyuki 東北大学, 電気通信研究所, 助教 (00570251)
• Project Period (FY): 2018-04-01 – 2022-03-31
• Keywords: 関数型プログラミング言語 / 表示的意味論 / 完全抽象モデル / プログラム検証 / 線形論理 / 量子プログラミング言語 / 圏論 / 交差型

Outline of Final Research Achievements

Our work provides useful models of programming languages equipped with complex computational effects in a general framework. Among these, the model of a functional quantum programming language analyzes a new aspect of the quantum computational effect. This semantic evolution opens many technical challenges, provides ideas to solve them, and makes great progress of the research area.
We also studied an application of our theoretical techniques to model checking, and obtained a new algorithm with an implementation.

Free Research Field

プログラミング言語理論

Academic Significance and Societal Importance of the Research Achievements

本研究で得られたプログラミング言語の表示的意味論の成果は，分野のまとまった成果を一般性を持って再構成するものであり，新しい長期的な視点を分野に提供するものであり，今後の意味論分野の発展に大きく寄与するものである．また量子計算の機構を備えた関数型プログラミング言語は今後ますます重要となるものであり，その意味論的成果は大きく社会に資する研究である．本研究の意味論的技術はモデル検査などへの応用も期待でき，ソフトウェア工学的にも価値の高い技術である．