システム・ソフトウェア研究部門の目標と成果

システム･ソフトウェア研究部門は「だれもが、いつでも、どこからでも、だれとで も、どんな情報でも」自由にしかもリアルタイムでコミュニケーションできるユビキ タス環境の構築を目的としている。そこで本部門は、通信とコンピュータを融合した 高度なシステム・ソフトウェア・コンテンツに関して高信頼・高機能ソフトウェアの 研究を行うソフトウェア構成研究室、新しいソフトウェアの基礎理論の研究を行うコ ンピューティング情報理論研究室、共生コンピューティングの研究を行うコミュニケ ーションネットワーク研究室、インタラクティブコンテンツを実現するための技術の 研究を行う情報コンテンツ研究室の４基幹研究室と情報社会構造研究室（客員）から 構成される。以下、基幹研究室における 2015 年度の研究活動成果の概要を述べる。

（１）ソフトウェア構成研究室

高信頼プログラミング言語の基礎理論および実装技術の確立、さらに基礎研究成果 を活かした次世代プログラミング言語の実現を目指し、理論と実践の両面から研究を 行ってきた。理論研究では、高水準なキーバリューアクセスを実現するための型理論 とコンパイル方式を構築し、ML 系高信頼言語から低レベルキーバリューストア上に、

レコードやリストなどのデータ構造が型安全に操作できる操作系が構築できることを 示すなどの成果をあげた。実践面では、本研究分野で推進している次世代高信頼プロ グラミング言語 SML#の開発を進め、完全な並行 GC を完成させ、６４ビット版ネイテ ィブスレッドサポート機能の開発などを行った。

（２）コンピューティング情報理論研究分野

書き換えシステムは、等式に基づく柔軟な計算と効率的な推論を与える数学的理論 である。本研究室では、書き換えシステムの基礎理論と定理自動証明、代数的仕様記 述、関数・論理型言語などへの応用について研究を進めている。本年度の主な研究成 果は以下のとおりである。(i) 項書き換えシステムに対する文脈移動変換法と文脈分 割変換法を提案し、これらの変換法を書き換え帰納法と組み合わせた新しい定理自動 証明システムを開発した。(ii) さまざまな証明手法に基づいて項書き換えシステム の合流性検証器 ACP の開発を進め、第 4 回合流性コンペティッション(CoCo 2015)にお いて第 1 位の成績を収めた。

（３）コミュニケーションネットワーク研究室

能動的情報資源の応用研究では、個人向き知識ベースの設計概念を新たに提案し、

その基礎的検討を開始した。具体的には、人々の種々の活動に関わる情報・知識の獲

得と構造化、及び、能動的情報資源として集積された記憶の活性・想起手法などにつ

いて検討した。知的ネットワークサービスの研究では、エージェントを活用したサン

ドボックス環境による安全なサービス個人化手法を提案し、プロトタイプを用いた実

験により、その有効性を検証した。更に、エージェント型 IoT（AIoT）に関する研究

システム・ソフトウェア研究部門

では、AIoT のシステム・コンセプトを新たに提案し、分散環境上の様々なデバイスに エージェント機能を装着して行われるデバイス知能化、AIoT デバイスの分散協調制御 方式などを検討し、プロトタイプシステムの試作と実験により AIoT の効果を確認した。

（４）情報コンテンツ研究室

人との相互作用によって新たな価値を創造するインタラクティブなコンテンツに関

して、それらを実現するさまざまな技術に関する研究に取り組んだ。まず、細かな手

指の動きを用いたインタラクションに向けて、磁気式の６自由度 3D トラッキングシス

テムを開発した。また、 「場」の状況を認識して快適なコミュニケーション空間を提供

する研究では、状況に応じて形状や位置を変化させることができるロボッティックデ

ジタルテーブルや壁型ディスプレイを試作し、それらが人の活動に効果的に作用する

ことを確認した。さらに、ロボットに対する人の心理的安心感のモデル化にも取り組

んだ。

システム・ソフトウェア研究部門

ソフトウェア構成研究室

次世代高信頼プログラミング言語の理論と実装

ソフトウェア構成研究分野 教 授 大堀 淳

＜研究室の目標＞

今実現しつつある高度情報化社会が，従来通りの信頼性と安全性を確保しながら発展していくた めには，高信頼ソフトを効率よく構築する技術の確立が必須である．高信頼プログラミング言語の 開発は，その中核をなす重要な課題である．そこで，当研究室では，高信頼プログラミング言語の 基礎理論および実装技術の研究，さらに，基礎研究成果を活かした次世代プログラミング言語の実 現を目指している．具体的には，これまでに我々の基礎研究によって得られたレコード多相性など の先端機能を装備した次世代高信頼プログラミング言語SML#の開発を進めるとともに，より堅牢 で信頼性の高いソフトウェア構築原理の確立を目指し，コンパイルの論理学的基礎の確立，低レベ ルコードの検証理論の構築，高信頼コンポーネントフレームワークのための型理論の構築などの基 礎研究を進めている．

＜2015年度の主な成果＞

１． SML#コンパイラの開発

SML#は，当研究室で設計・開発している高信頼プログラミング言語であり，以下の特徴を持つ．

(1) 多相型レコード演算やランク１多相性等の先端機能を初めて実現，

(2) Cなどの既存言語やデータベースなどのシステムとの高い相互運用性，

(3) Standard MLと上位互換性を持つ．

これらの特長およびSML#コンパイラに含まれる諸機能は，我々の基礎研究成果によって可能とな SML#プログラム

アプリケーション 関数型

高信頼言語

OS・ライブラリ

データベース

実行時型エラー

柔軟性の欠如

インターフェースの 不整合

型システムによる静的検査

多相レコード計算

OS・ライブラリ データベース 型安全な多相型FFI

図１：SML#による高信頼言語と既存言語を統合した次世代プログラミング環境の実現

システム・ソフトウェア研究部門

った最先端のものと評価されている．

本年度の主な開発項目は完全な並行GCの開発である．次世代のソフトウェア開発の生産性と信 頼性の向上に寄与すると期待される関数型言語の課題は，マルチコア上で動作するネイティブスレ ッドのサポートである．この最大の障害は，実用的な並列化技術が未熟なゴミ集め（GC）方式に あった．本研究では，スレッドと完全に並行に動作する GC の理論と実装方式を開発し，SML#コ ンパイラに実装した．このGCは，従来困難であった，高信頼言語におけるマルチコア上のネイテ ィブスレッドのサポートに道を拓くものである．３月に，このGCを含むSML#3.0.0版をリリース した．

２． 高水準なキーバリューアクセスの型理論とコンパイル方式．

ストレージやクラウド基盤のインターフェイスとして広く使用され始めた従来のキーバリュー ストアは，プログラミング言語が提供するレコードや配列などの構造を持たない低レベルな機能に 制限されていた．本研究では，名前に過ぎないキー集合を使って，高水準なデータ構造を表現する ための型理論とそのコンパイル方式を構築し，キーバリューストアの型安全かつ高水準のアクセス を実現する方式を確立した．（論文[1]）

３．外部データ形式 JSON を高水準言語に統合する理論と実装方式の構築．

インターネット上でデータを送受信するフォーマットとして広く使用され始めた JSON を安全か つ高水準に操作する型理論と実装方式を開発し，高水準言語から JSON を安全にシームレスに操作 する方式を確立した．この成果は，オブジェクト指向プログラミング言語の最高峰の国際会議であ る ECOOP2016 に採録され，2016 年 7 月に発表予定である．（論文[3]）

＜職員名＞

教 授 大堀 淳（2005年より）

助 教 上野 雄大

＜プロフィール＞

大堀 淳 １９５７年生．１９８１年東京大学文学部哲学科卒業．同年沖電気工業（株）入社．１９８ ９年ペンシルバニア大学大学院計算機・情報科学科博士課程修了．Ph. D．その後，英国王立協会特別研 究員（グラスゴー大学），沖電気工業（株）関西総合研究所特別研究室長，京都大学数理解析研究所助 教授，北陸先端科学技術大学院大学教授を経て，２００５年４月より東北大学電気通信研究所教授．プ ログラミング言語およびデータベースの基礎研究に従事．１９９６年第１０回日本ＩＢＭ科学賞受賞．

＜ 2015 年度の主な発表論文等＞

[1] Katsuhiro Ueno, Atsushi Ohori. A Type Safe Access to Key-value Stores from Functional Languages. Journal of Information Processing, Vol. 24, No. 1, pp.141-151, 2016.

[2] Katsuhiro Ueno, Atsushi Ohori: A foreign language interface from ML to shell. New Generation Computing, to appear.

[3] Atsushi Ohori, Katsuhiro Ueno, Tomohiro Sasaki, Daisuke Kikuchi: A Calculus with Partially Dynamic Records for Typeful Manipulation of JSON Objects. In Proceedings of the 30th European Conference on Object Oriented Programming (ECOOP 2016), 24 pages, to appear.

システム・ソフトウェア研究部門

コンピューティング情報理論研究室

計算と証明の融合によるソフトウェア構成原理

コンピューティング情報理論研究分野 教 授 外山 芳人

＜研究室の目標＞

本研究室では、証明と計算を融合した新しいソフトウェアの構成原理について研究している。ソフトウェ アの形式的開発や検証では、ソフトウェアの効率のみでなく、その論理的な正当性も問題となる。書き換え システムを基礎とした計算・証明モデルは、証明の世界と計算の世界を統一的な枠組みで取り扱えるため、

新しい構成原理に基づくソフトウェアの実現が可能である。我々は、書き換えシステムに基づく関数型言語 を対象に、与えられたプログラムから効率的なプログラムへの自動変換、仕様からのプログラム自動合成な どの基礎研究を行っている。さらに高階書き換えシステム、プログラムの帰納的性質の自動証明法、関数・

論理型言語と定理自動証明システムの融合など、書き換えシステムに基づく計算・証明パラダイムの理論的 および実験的研究を進めている。

研究テーマ

（１） 書き換えシステムの基礎理論 （３）関数・論理融合型言語

（２） プログラム検証・変換・合成 （４）定理自動証明システム

＜2015 年度の主な成果＞

1. 合流性自動証明法の研究

項書き換えシステムの永続性と型情報を利用した新しい合流性証明法に基づいた新しい合流性自動証明 手法を提案し、本研究室で開発している合流性自動証明システム ACP へ提案手法を組み込んだ。さらに、帰 納的定理自動証明法に基づく基底合流性判定手法を提案し、実験をとおしてその有効性を確認した。

2. 検証のためのプログラム変換の研究

自動検証を目的としたプログラム変換法である文脈移動法が、項書き換えシステムの自動変換にも有効で コンピュータが扱う多くの問題では『証明の世界』と『計算の世界』の間に自然な結び付きがあります。

この結び付きをうまく用いることによって、専門知識のない人でも簡単に利用できる自動証明システム やプログラミングシステムが実現できます。