2022 Fiscal Year Final Research Report
Staged Computing based on Advanced Type Systems
Project/Area Number |
18H03218
|
Research Category |
Grant-in-Aid for Scientific Research (B)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Review Section |
Basic Section 60050:Software-related
|
Research Institution | University of Tsukuba |
Principal Investigator |
|
Co-Investigator(Kenkyū-buntansha) |
浅井 健一 お茶の水女子大学, 基幹研究院, 教授 (10262156)
Kiselyov Oleg 東北大学, 情報科学研究科, 助教 (50754602)
|
Project Period (FY) |
2018-04-01 – 2022-03-31
|
Keywords | プログラム生成 / 多段階計算 / 型システム / 型安全性 / モジュール / 計算エフェクト / 異種プログラム生成 / プログラムの信頼性 |
Outline of Final Research Achievements |
Multi-stage programming is a means to generate programs by programs, by specializing a program by parameters or computation environments. Although it has been used in various application fields, there are many advanced features used in these applications which are not guaranteed to be safe or reliable. This research project aims to ensure the safety and reliability of generated programs. We have obtained a calculus for type-safe generation of modules, type systems for control operators that are proven sound, and a rigid formulation of heterogeneous program generation.
|
Free Research Field |
プログラム生成、関数型プログラム言語と型理論
|
Academic Significance and Societal Importance of the Research Achievements |
本研究の学術的な意義は、従来の多段階計算の限界を突破して、現実に必要とされる広い範囲の言語機構に対する「型安全なプログラム生成」を保証するために必要な型理論的基礎を構築したことである。具体的には、モジュールのコードの生成、代数的効果、異種プログラム生成などに対応し、かつ、型安全性を保証された多段階計算体系は、オリジナリティが非常に高い研究であると考えている。 社会的意義については、MetaOCaml言語における異種プログラム生成機能の実装や、高性能ソフトウェアラジオの実装などがあげられる。
|