2015 Fiscal Year Annual Research Report
Haskellコアの意味論－先端的ソフトウェア検証基盤へ向けて
| Project/Area Number |
25540002
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
浜名 誠 群馬大学, 大学院理工学府, 助教 (90334135)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
勝股 審也 京都大学, 数理解析研究所, 助教 (30378963)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / 圏論 / 関数プログラム / 情報学基礎 / Haskell |
|---|
| Outline of Annual Research Achievements |
本年度はコアHaskellのモデルの一つとして代数理論から操作的意味論の抽出のために、代数理論と書換え系を研究した。
特にHaskellのグラフ簡約のメカニズムのモデル化のために、グラフ構造の代数化を行った。BloomとEsikによるイテレーション理論を援用し、グラフ間の等式による完全な公理化と、トレース圏を含むようなイテレーション圏を用いた圏論的意味論を与えた。これによりグラフ構成子を圏論的構成として理解することが可能となった。結果としてグラフの等価性に対する健全かつ完全な等式論理を得ることに成功した。
さらに計算効果の代数的モデルとして、モナドの研究として、余稠密モナドの概念を使い、ファイブレーションの基礎圏から全域圏へのモナドの持ち上げの結果を得た。これは従来の圏論的TT-リフティングではカバーできない例を含むため、Hakellのモナド型のための述語のモデル化への応用が期待できる。
また、Haksellの計算モデルの一つとして有望である高階書換え系のチュートリアルの講師をドイツでの国際サマースクール ISR 2015 にて行い、国際的な研究者、学生に書換えモデルの有用性と理論を教授した。さらに日本ソフトウェア科学会 第18回プログラミングおよびプログラミング言語ワークショップにおいて、Haskellを代表とする関数型プログラミング言語と書換え系の関係についてのチュートリアル行い、好評を博した。これは、PPL 2016発表賞を受賞した。
|
