| Project/Area Number |
16K00095
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
|
|---|
| Research Collaborator |
Tanaka Kazunari
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2018: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 型システム / 中間言語 / 型検証 / プログラム検証 / 型健全性 / プログラミング言語処理系 |
|---|
| Outline of Final Research Achievements |
I did several researches to strengthen the robustness of the OCaml type checker. Aiming at improving the theoretical foundation and structure of the type checker, I first solved the question of the interaction between GADTs (generalized algebraic datatypes) and the exhaustiveness check of pattern matching, both theoretically and practically. I worked with other developers at making the type checker more modular. I studid the conditions for improving the safety of the language through a typed intermediate language. I also worked on several topics of program verification, which should help with the formalization of this typed intermediate language.
|
| Academic Significance and Societal Importance of the Research Achievements |
社会のあらゆる所でソフトウェアは我々の生活をサポートしている。娯楽や書類の作成から、飛行機の飛行制御システムや医療機器まで、応用は幅広いが、その全ての場面で安全性が求められる。型システムがプログラムの安全性の確保に効果的であり、型の表現力が高いほどの効果が現れる。しかし、型システムが複雑になると、型の整合性の確認を行う型検証器とその後の処理の正しさの担保が難しくなる。この研究はプログラミング言語処理系の型の正しさを保証することでソフトウェアの安全性の向上を目指す。
|
