2014 Fiscal Year Annual Research Report
| Project/Area Number |
25280024
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
馬谷 誠二 京都大学, 情報学研究科, 助教 (40378831)
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | プログラミング言語 / ソフトウェア契約 / 計算効果 / プログラム検証 / ゲーム意味論 |
|---|
| Outline of Annual Research Achievements |
今年度設定した3つの研究課題(1)計算効果を持つ言語機構とソフトウェア契約の統合，(2)ハイブリッド契約検査技術の代数的データ型への適用，(3)ソフトウェア契約の代数的意味論の確立，について取組み，以下のような成果をあげた．
(1) 計算効果を持つ言語機構とソフトウェア契約の統合: 昨年度の研究で構築したshift/resetを使った限定継続機構を導入した契約計算体系の意味論を見直し，まず限定継続機構を除去するCPS変換を定義し，その意味論を引き戻すことで新しい意味論を得た．また，この意味論から導出できるプログラムの等価性がCSP変換を通じて健全であることを証明した．古い意味論にあった，契約違反が生じた時のblameの非自明な部分も，新しい意味論では直観的には理解がしやすいものになっているが，この直観を形式化することがまだ課題として残っている．
(2) ハイブリッド契約検査技術の代数的データ型への適用: 昨年度の研究で構築した代数的データ型に対するハイブリッド契約検査の枠組みについて，プログラミング言語分野で最も権威のある国際会議のひとつである ACM POPLで成果発表を行った．また，今年度計画していた，この枠組みの欠点のひとつであるデータ型間のキャストの際に生じるコンストラクタ変換のコスト削減手法の考案については，まだ，あまり成果がないが，その後予定される本格的な検証実験の準備として，並行して，計算体系の実装をOCamlコンパイラを改造することで進めた．
(3) ソフトウェア契約の代数的意味論の確立: 昨年度までに目処をたてた，単純型付ラムダ計算に単純な契約を付加した体系に対するトレース意味論を構築し，Findler-Felleisen流の契約に対する操作的意味論とある意味で一致することを証明した．また，付加的結果として，この意味論が文脈等価性と呼ばれるプログラム等価性に対し完全抽象的(fully abstract)であるという予想もほぼ証明できている．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で述べた3つの課題について、交付申請書で計画した通りに進んでいる．処がたっている。(2)での，データ型間のキャストの際に生じるコンストラクタ変換のコスト削減手法については，具体的な成果がでていないが，検討を進めていく段階で，問題解決には様々なアプローチと付帯的な問題があることがわかったためその利害得失を見極めている段階である．
|
| Strategy for Future Research Activity |
現在までおおむね順調に進んでおり、交付申請書・研究実績の概要であげた3課題についての研究をそのまま進めてゆく。(1)と(2)の課題については1人以上の大学院生の研究協力を見込める体制が整ったため、それを梃子にして研究を推進していく。研究計画の変更は特に考えていない。
|
| Causes of Carryover |
最終年度に契約計算のコンパイラ実装を進めるにあたって、研究者の人件費を確保するため。
|
| Expenditure Plan for Carryover Budget |
平成27年9月博士課程修了者をポスドク研究員として年度後半に雇用することを計画している。
|
-
[Journal Article] Manifest Contracts for Datatypes2015
Author(s)
Taro Sekiyama, Yuki Nishida, Atsushi Igarashi
-
Journal Title
Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
Volume: 1
Pages: 195-207
DOI
Peer Reviewed / Acknowledgement Compliant
-
-
-
-
-
-
[Presentation] Manifest Contracts for Datatypes2015
Author(s)
Taro Sekiyama, Yuki Nishida, Atsushi Igarashi
Organizer
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Place of Presentation
Mumbai, India
Year and Date
2015-01-15 – 2015-01-17
-
-
-
