2013 Fiscal Year Annual Research Report
新パラダイム計算をねじふせる―多様な意味論的手法の合同・発展・応用
| Project/Area Number |
24680001
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
蓮尾 一郎 東京大学, 情報理工学(系)研究科, 講師 (60456762)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Keywords | プログラム理論 / 形式検証 / 量子計算 / ハイブリッドシステム / 応用数学 / 国際研究者交流（フランス） / 国際情報交換（イタリア） / 国際情報交換（オランダ） |
|---|
| Research Abstract |
本研究の目標たる新パラダイム計算の研究のうち，特に獲得目標として挙げた量子プログラミング言語とハイブリッドシステムの研究について，想定以上の成果を得た．
まず量子プログラミング言語の研究においては，線形論理に基づいた proof net による量子計算の表現について学生・海外研究者と共に研究を行い，論文２報がプログラミング言語研究分野のトップ会議 ESOP 2014 と理論計算機科学分野のトップ会議 CSL-LICS 2014 にそれぞれ採択された．さらに，これらの論文で用いた相互作用の幾何とよばれる手法の，状態遷移系の圏論的抽象化たる余代数を用いた一般化について学生・国内研究者と共に研究を行い，この論文も CSL-LICS 2014 に採択された．特に後者の論文で樹立された一般論は，（量子計算的効果を含む）多様な計算効果に対して一挙に低レベル実装を与えるものであり，本研究の目標たる量子プログラミング言語処理系の実現に向けての大きな理論的前進である．
またハイブリッドシステムに関しては，産業界の共同研究相手からもたらされたテストケース生成問題に対し，プログラム論理を利用して検索空間を大きく削減する手法を学生・国内研究者と共に研究し，論文がハイブリッドシステムに関する国際ワークショップ HAS 2014 に採択された．この成果については特許出願中である．
さらに，より広い文脈での状態遷移システムとその余代数モデリングについて，仕様を記述するための様相論理のもつ圏論的構造について研究を行い，論文１報がプログラム意味論分野の国際会議 MFPS 2013 に採択され，また，論文もう１報が余代数の国際ワークショップ CMCS 2014 に招待論文として採択された．これらの成果のさまざまな応用（特に量子計算・量子通信分野における応用）が今後期待される．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
量子プログラミング言語について，技術的困難を線形論理や余代数など他のトピックを援用する形で解決し，理論的ブレイクスルーを得た．またハイブリッドシステムについては産業界との協働が当初予想しなかったスピードで進みつつある．余代数の理論による基礎固めも当初計画より進展している．
|
| Strategy for Future Research Activity |
平成25年度の研究において得られた理論的ブレイクスルーを，本研究の具体的獲得目標（特に量子プログラミング言語の処理系）に落としこむ．同時に理論的基礎の幅広い発展を図る．
|
| Expenditure Plans for the Next FY Research Funding |
研究の一端を担う学生たちがいまだ修士課程であったので，成果発表等に伴う旅費が少なくなった．
これらの学生たちの多くは次年度の国際会議に論文がすでに採択されており，この旅費として使用する．
|
