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
|
| Project Status |
Completed (Fiscal Year 2022)
|
| Budget Amount *help |
¥12,740,000 (Direct Cost: ¥9,800,000、Indirect Cost: ¥2,940,000)
Fiscal Year 2021: ¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2020: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2019: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Fiscal Year 2018: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
|
|---|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究の学術的な意義は、従来の多段階計算の限界を突破して、現実に必要とされる広い範囲の言語機構に対する「型安全なプログラム生成」を保証するために必要な型理論的基礎を構築したことである。具体的には、モジュールのコードの生成、代数的効果、異種プログラム生成などに対応し、かつ、型安全性を保証された多段階計算体系は、オリジナリティが非常に高い研究であると考えている。
社会的意義については、MetaOCaml言語における異種プログラム生成機能の実装や、高性能ソフトウェアラジオの実装などがあげられる。
|
Report
(5 results)
Research Products
(53 results)
