• 電源を切ってもデータを記憶し続ける不揮発性デバイスを、メモリだけでなく、CPUなどの演算器やシステム全体の構成に積極的に活用する回路・システム構築方法が「不揮発性ロジック」です。本テーマでは、不揮発性デバイスに「回路構造情報」を記憶することで、製造プロセス（P）や電源電圧（V）、温度（T）などに起因する回路特性バラつきに対して頑健な回路を、少ないオーバーヘッドで実現できる回路構成を提案しています。

この成果は、今後微細化が益々進行する超微細LSI の高信頼化・高性能化に大いに寄与する技術であり、これに関連する分野で有意義な共同研究ができるものと考える。

• 脳が特異的に持つ機能（例えば、意識/無意識過程、自己、選択的注意など）を、これまでの情報科学的な方法とは異なり、デバイスの物理的な特性・ダイナミクスを用いて直接的に構築することにより、小型高効率高性能な脳型ハードウェアの開発を行う。具体例としては、カオスニューラルネットワークリザバー、高次元複雑ダイナミクスによる最適化、スピン軌道トルクデバイスによるニューラルネットワーク等である。

この脳型ハードウェアは、ユーザ個人の情報の学習が必須なエッジ端末に有効で、例えば、補聴器や入れ歯に内蔵して心電や脳波、唾液成分などの学習により、異常検知を行う見守りデバイスなどへの応用が期待できる。

• プログラムの効率の改善や形式的検証に関する研究を行っている。短期間で記述したプログラムは実行時間やメモリ使用量について非効率的であることが多いが、この問題に対し、プログラム変換によって機械的に改善する手法の開発に取り組んでいる。また、大規模なプログラムはその複雑さから予期せぬバグを含みやすいが、この問題に対しては、プログラム検証やモデル検査とよばれる数学的手法によって実行前に網羅的に検証する研究も進めている。

通常のソフトウェア開発では有限個のテストを通じて動作確認が行われるが、モデル検査器や定理証明支援系などのツールを用いることで、無限個の入力に対して動作が保証されたプログラムの作成を実現できる。

• プログラミング言語および計算モデルに関する世界最先端の研究を行っている。特に、二つのプログラムの動作が等しいという「プログラム等価性」の一般的証明手法や、近年再注目されている「関数型プログラミング」、「軽量形式手法」とも呼ばれる「型システム」等に関する研究・普及活動を行い、大手電機メーカー技術者らとの訳書「型システム入門」は理論的専門書としては異例の大手インターネット書店プログラミング入門書2 位となった。

ソフトウェア、特にDSL（ドメイン特化言語）を含むプログラミング言語およびツールの設計・開発。関数型プログラミング、型システムないし形式手法の導入・利用。

• 不特定多数のユーザ端末が供出する空きストレージとブロックチェーンを活用して、高度な安全性を実現するP2P型ストレージの構築技術を開発しています。構築ストレージは、中央管理サーバの問題に起因する保存データの大規模情報漏洩リスクも回避可能です。また、暗号通貨を報酬と利用料に使用し、全ユーザの公平なストレージ利用も実現します。さらに、実用的なデータ商取引を可能にするスマートコントラクト技術も開発しています。

ブロックチェーン技術を活用したスマートコントラクトやフィンテックなどのBitcoin2.0 型アプリケーション、モノインターネット（IoT）、医療情報データベース関連などの開発を行う企業との共同研究を希望します。