| 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
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2016: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究成果は、経験と試行錯誤が頼りであった交差型システムの設計に、数理的な背景を見出したことである。数理的な背景とは、具体的には、ゲーム意味論と組合せ論である。ゲーム意味論は多くの研究があるものの、成果を理解し利用できる研究者の数が少ないという問題があったが、本研究成果によってゲーム意味論の知見を交差型システムの形で幅広い研究者に理解できる形で提供できる道が拓けた。また組合せ論との関わりを示したことで、交差型システムに新しい見方を提供し、例えば母関数などといった組合せ論の概念を交差型システムについて考えることを可能にした。
|
