表現力が高く安全に相互運用可能なプログラミング言語の理論と実現
| Project/Area Number |
10J06019
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
伊奈 林太郎 京都大学, 大学院・情報学研究科, 特別研究員(DC1)
|
|---|
| Project Period (FY) |
2010 – 2012
|
| Project Status |
Completed (Fiscal Year 2012)
|
| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2012: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2011: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2010: ¥700,000 (Direct Cost: ¥700,000)
|
|---|
| Keywords | プログラミング言語 / 安全性 / 型理論 / 動的型 / 相互運用 / 停止性 / 型安全性 |
|---|
| Research Abstract |
[研究目的]
ソフトウェアプログラムは,安全に実行できる信頼性が要求される一方で,コストを抑えるために迅速かつ柔軟に開発する必要がある.前者の実現のために,型理論の成果を用いた静的型付け言語がプログラミング言語として広く用いられている一方,後者を優先する場合は動的型付け言語が用いられる場合が多く,どちらを用いるかは開発を開始する段階で決めねばならず,途中で変更することができない.そこで本研究では,柔軟な開発を可能にする動的型付け言語の特性と,安全性を保証する静的型付け言語の特性を併せ持ち,これらの特性を開発の段階やソフトウェアプログラムの部位によって使い分けることができる言語を提案する.これにより,柔軟かつ安全なソフトウェアプログラムの開発が可能となる.
[研究成果]
前年度までに,Javaを拡張し静的型付けと動的型付けを混在できる言語のための数学的なモデルが得られていたが,実際の処理系を実装するためのアルゴリズムの一部が欠けていた.具体的には,より詳細な型がよりおおまかな型に含まれることを表す部分型という関係を検査する必要があり,前年度までに提案した手続きではジェネリクスを含む場合に停止することが示せていなかった.本年度はこの手続きの停止性を証明することに成功し,部分型検査のためのアルゴリズムを完成させることができた.この成果については前年度までの成果とともに雑誌論文として発表する予定である.また,ジェネリクスを含まない簡略化された言語に関しての実装も進めた.
|
Report
(3 results)
Research Products
(3 results)
-
-
[Presentation] Gradual Typing for Generics2011
Author(s)
Lintaro Ina
Organizer
The 2011 ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Place of Presentation
アメリカ・オレゴン州・ポートランド
Year and Date
2011-10-26
Related Report
-
