萩谷研究室では、
計算機ソフトウェアに関する理論的な考察から、そのような 理論的考察の結果に基づいたソフトウェア・システムの開発
に至るまで、幅広 い研究活動を行っています。

関数プログラミング

本研究室では、型理論、カテゴリー理論、線形論理などの論理学の進んだ概 念を応用して非手続き的な言語の基礎付けを行うことに興味を持っています。 特に、型付きλ計算の枠組を用いて関数プログラミングの研究を行なっていま す。

また、関数プログラムの変換や導出にも興味があります。この分野における 最近の研究としては、構成子の特化と関数のベクトル化があります。どちらも データ型の変換に関するものです。

定理証明と証明検査

計算機上に形式的な証明を作成することは、計算機科学における形式的手法 の基礎となっています。本研究室では、計算機ソフトウェアの正当性の証明だ けでなく、数学の種々の分野を形式化することにも興味を持っています。この 研究分野は最近では形式的数学と呼ばれています。 本研究室では、主として次のような観点から定理証明と証明検査の研究を行っ ています。

直観に依存した数学的概念の形式化:

人間の直観に依存しているために十分に公理化されていない数学的概念を形 式化することに興味を持っています。例えばグラフの平面性は通常、直観的 に非形式的に理解されています。そのような概念を、定理証明系や証明検査 系を用いて定理の証明を容易に自然に行えるように形式化することが重要で す。

数学的思考の過程における定理証明系の利用:

既に得られた定理を検査するためだけに定理証明系を利用するのではなく、 形式的理論を構築する過程全体の中で活用することが重要だと考えています。 特に、定理や補題を発見したり修正したりする過程で定理証明系を利用する ことが重要です。人間の数学的思考能力と証明系の計算能力をスムーズに協 調させるには、人間と定理証明系の間のユーザ・インターフェースを改善す る必要があります。

ユーザ・インターフェース

ユーザ・インターフェースの分野における本研究室の興味は主として、プロ グラムや証明を書くような人間の思考過程を支援する計算機環境を開発するこ とにあります。この目的のために、本研究室では、 CAEP(Computing-as-Editing Paradigm)と呼ぶパラダイムを提唱しています。 このパラダイムは、種々の計算をテキスト・エディタを用いた文書編集の過程 と統合させようとするものです。

ゲノム情報

最近に萩谷昌己が文部省のゲノム情報のプロジェクトに参加していることよ り、計算機ソフトウェアの観点から生命の理解を深めようとする試みも行って います。

本研究室では、生物系のモデリングとシミュレーションの研究を行っていま す。特に、遺伝子発現制御、シグナル伝達、代謝などのモデリングやシミュレー ションに興味を持っています。本研究室の目標は二つあります。一つは、生物 系のモデリングとシミュレーションのための新しい方法論を開発すること。も う一つは、計算機ソフトウェアのような人工物との比較のもとでシステムとし ての生物の理解を深めることです。

戻る


<vu@is.s.u-tokyo.ac.jp>

Last updated on Thursday, 3 1997