Game semantics and intersection type systems for program verification

2018 Fiscal Year Final Research Report

• Project/Area Number: 16K16004
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: The University of Tokyo
• Principal Investigator: Tsukada Takeshi 東京大学, 大学院情報理工学系研究科, 助教 (50758951)
• Project Period (FY): 2016-04-01 – 2019-03-31
• Keywords: ゲーム意味論 / 交差型システム / generalised species / 線形論理

Outline of Final Research Achievements

With growing concern about reliability of software systems, functional programming languages and their strong type systems are drawing attention. Each type system describes and ensures different properties of different programming languages, and one needs to design a type system that fits one's purpose. This research project focuses on a special class of type system, called intersection type system, and develops a general method for designing intersection types for a variety of languages. The method is based on game semantics, a mathematical framework for giving interactive semantics of programs.

Free Research Field

プログラム意味論

Academic Significance and Societal Importance of the Research Achievements

本研究成果は、経験と試行錯誤が頼りであった交差型システムの設計に、数理的な背景を見出したことである。数理的な背景とは、具体的には、ゲーム意味論と組合せ論である。ゲーム意味論は多くの研究があるものの、成果を理解し利用できる研究者の数が少ないという問題があったが、本研究成果によってゲーム意味論の知見を交差型システムの形で幅広い研究者に理解できる形で提供できる道が拓けた。また組合せ論との関わりを示したことで、交差型システムに新しい見方を提供し、例えば母関数などといった組合せ論の概念を交差型システムについて考えることを可能にした。