萩谷研究室 先生アンケート


回答者:萩谷昌巳先生

Q 現在、どのような研究をなさっていらっしゃるのですか?

本研究室では、計算機を用いた演繹的推論に関する研究を行っています。計算 システム(ソフトウェア、ハードウェア、プロトコルなど)の検証、自動演繹 (定理自動証明)、そのための理論的な枠組(論理体系や意味論)などの研究を行 っています。また、プログラミング言語の分野では、主として関数プログラミ ングの研究を行って来ました。関数プログラミングの研究は、演繹的推論を計 算機上に実装するためのプログラミング言語としての関数型言語の研究、およ び、演繹的推論の側面を持つ効率化手法である関数プログラムの変換・部分計 算の研究、として位置付けることができます。また、演繹的推論を行うための ユーザ・インタフェースも重要だと考えています。

なお、演繹的推論とは独立に、広くユーザ・インタフェースの研究を行なって いる学生もおります。

それともう一つ、ゲノム情報、もしくは、より広い「生命情報」という流れが あります。これは上記の研究とはいまのところ関連はありません。萩谷は1991 年よりゲノム情報の研究を行っています。ゲノム情報は一言でいうと情報処理 の技術を応用して生物の研究、特に、遺伝子の解析を進めようとするものです が、最近では、その逆に、DNA等の生体高分子の機能を利用して分子レベルの 並列性と集積度を持つ計算機を作ろうという動きがあります。人工生命と同様 に、構成的な手法で生物もしくはその構成要素に迫ろうとする研究分野で、萩 谷も、生物化学や生物物理の先生方と共同でこの分野の研究を始めたところで す。

Q 研究室で行われているプロジェクトについて教えて下さい。

現在行われている研究プロジェクトは以下のようです。

*高階論理を用いたグラフ探索アルゴリズムの検証

高階論理の証明支援系(HOL)を用いて、グラフ探索アルゴリズムの検証を行っ ています。グラフ探索は最短経路問題などへの応用とともに、機械的な検証手 法の基礎としても重要です。本研究では、種々のグラフ探索アルゴリズムの正 しさを証明支援系を用いて統一的に系統的に検証することを目指しています。

*モデル検査を用いた並列ゴミ集めの検証と新アルゴリズムの発見

並列ゴミ集めは典型的な並行プログラムであり、その正しさは自明ではありま せん。本研究では、モデル検査の手法を用いて、ある程度機械的に並列ゴミ集 めのための種々のアルゴリズムを検証することを目指しています。特に、抽象 解釈とモデル検査を融合した抽象モデル検査という手法を用いています。また、 アルゴリズムを検証するだけでなく、新しい(正しい)アルゴリズムを発見する 試みも行っています。

*Javaセキュリティ

ネットワーク上のセキュリティを保証することは検証の分野で重要な研究テー マとなっています。特に、Javaに関するセキュリティが活発に研究されていま す。本研究室でも、これまでに、バイトコード検証とクラスローディングに研 究を行って来ました。

*紙インタフェース

紙の利点と計算機の利点を融合したユーザ・インタフェースの研究を行なって います。この研究は、実世界指向インタフェースの研究の一貫と考えることが できます。

*分子計算

上述しました。

 

〔トップページへ〕 〔「研究室紹介」のindexページへ〕
<vu@is.s.u-tokyo.ac.jp>

Last updated on 29 May, 1999