Programming Logic Group
プログラム論理研究室


卒業研究生募集

研究室紹介は、2016/10/19 (水) 15:15からと、 2016/10/24 (月) 12:15からです。
場所は、総合研究棟B-1027です。 「少しだけ覗いてみよう」という人も歓迎します。
情報学類WORD誌の研究室紹介はこちらです。
コンピュータサイエンス専攻パンフレットの研究室紹介はこちらです。


概要


研究内容

「ソフトウェアの正しさの保証」が大目標です。 そのために、(1)プログラム言語に対する理論を展開して正しく 効率良いプログラムを作るための研究を行い、 また、(2)作成されたソフトウェアをモデル検査や定理証明の 手法により検証する研究を行っています。

  1. プログラム言語論(職人芸プログラミングを科学的なプログラミングへ)
    •  ラムダ計算と型システムに基づくプログラム言語の体系
      今日の先進的なプログラム言語(たとえば、ML や Ruby) の中核には、 関数と型システムがあります。これらの性質を研究することにより、 プログラム言語の本質が見えてきます。 また、型システムと論理の関係を解明することにより、 プログラム合成の基礎が得られます。 そこで、ラムダ計算(関数)と型に基づいたプログラム言語の研究を行っています。
      • 研究テーマの例: 「制御機構(コントロール機構)に関する型システム」、 「精密な制御機構をもつ型つきプログラム言語の設計」、 「環境を扱うプログラム言語の設計」、「並列計算・モバイル計算への応用」など。

         

    • プログラム変換とメタプログラミング(マルチステージプログラミング)
      メタプログラムとは、 「プログラムを入力として受け取ったり、生成したプログラムを返したりするプログラム」のことです。 このようなメタプログラムは、実際には、いたるところで使われていますが(例:webアプリケーション), その正しさを一般的に保証する仕組みはまだあまり研究されていません。そこで、 メタプログラムの一種として、いくつかのプログラム変換を取り上げ、効率的で正しい変換について研究しています。
      • 研究テーマの例: 「部分計算(プログラム特化)の方法によるプログラム変換」、 「効率的なCPS変換(コンパイラで使われる変換)」、 「部分計算システムの実装・構築」

  2. ソフトウェアの検証(プログラムや設計書に究極の保証を与える)
    • モデル検査による検証

      モデル検査は、有限状態のシステム(ソフトウェア、ハードウェア、そのほか)が, 仕様(そのシステムが満たすべき性質)を満たすことを網羅的な探索により示す手法であり、近年の 計算パワーの上昇により, 非常に広い範囲のシステムの検証に用いられている「ホット」な話題です。 非常に状態数の多いシステムへの対処、 無限状態システムへの対処、実時間の記述、等々の拡張が待たれています。

      • 研究テーマの例: 「モデル検査による並列アルゴリズムの検証」、 「効率的な実時間モデル検査の研究」、 「モデル検査システムや定理証明システムのユーザインターフェースの作成」 など。
    • プログラム論理の体系と定理証明 モデル検査は高速に処理ができる方法ですが、処理しきれない精密な仕様も存在します。 そのような場合、数学的な定理を証明するような形で、コンピュータ上でソフトウェアの性質を検証するのが 「定理証明』の手法です。 ここでは、様々なプログラム言語や論理体系を統一して記述し、 共通する性質を記述したり推論するための論理体系を構築し、 その上で、自動または手動で定理証明が可能な範囲を見つけだすことを目的として研究を行っています。
      • 研究テーマの例: 「論理フレームワークによるプログラム変換の定式化」、 「時相論理(モデル検査で使う論理)における自動的な定理証明」
          

学生に望む態度

課題が与えられるを待っているのではなく、 自主的に新しいテーマを開拓する意気込みをもつ人、 「手を動かす」だけや「頭を動かす」だけでなく、 「手も頭も動かす」人を期待します。


セミナー

研究室のセミナーは、原則として週1回、半日を費やし てとことん議論します。 それ以外には教員と学生の個別のミーティングを随時行います。

内容は、春学期は、文献(ソフトウェア基礎関係の英文の本)の輪講、 秋学期は各自の研究テーマに沿った論文紹介もしくは研究報告です。

なお、セミナー以外の拘束時間は最小限にして、 学生の自主性を重んじる方針です。


知っておくと良い科目

プログラム言語と論理が基本となります。 これについては、以下の科目を学んでおくと良いでしょう。 ただし、これらの科目の履修が必須というわけではなく、 研究室配属後の輪講では、前提知識を仮定せずに勉強します。 研究にあたって一番大事なことは「やる気」です。 やる気さえあれば研究室配属後に不足している知識を補うことができます。 また、研究の材料を発掘するためには、情報学全般にわたって好奇心をもって接する態度が望まれます。


文献

まず最初に読むとすると以下のいずれかが良いでしょう。 詳しい参考文献リストはここにあります。


研究室生活について


進路

これまでの在籍者の進路は、 学類からは13人中10人が大学院進学です(他大学の大学院進学の2人を含む)。
大学院修了後の進路は、NTT、NEC, 大日本印刷、三菱電機、楽天などです。


研究設備

学生1人あたり、1台のデスクトップPCと1つの広い机を確保します。

図書はまだまだ整備中です。インターネット時代になっても良質の出版物の 重要性は残りますから、本をどんどん買いたいと思っています。


備考

基礎理論について:

ソフトウェアの理論は難しいと言われます. 論理など数学的な道具立てを用いて深い理解を追求するので, とっつきにくい事がその原因でしょう.しかし,苦労なしに人より抜きん出ることはできません. 今,ソフトウェアの世界では、論理がわかる人に対する 需要が高まっています. プログラミングを初めとする情報学の幅広い知識を身につけた皆さんが、次にやるべきことは, 1点か2点に絞って「深さ」を追求することです。プログラミングの仕組みを論理的に説明する 理論を知り、それを生かしたソフトウェアを作ることは、皆さんの知的好奇心を大いにくすぐる 格好の題材になると思います。

誰でも書けるプログラムを素早く大量に書く能力より, 正しさを保証しやすいプログラムを書く能力や、プログラムの正しさを理解す る(そして、可能ならば正しさを示す) 能力を身につけてください. 当研究室は,プログラムや論文の「数」や「量」を誇りたい人には向きません. 質の高い仕事を1つ1つ達成したい人向けです.

プログラミングについて:

プログラミングを「がんがん」できることに越したことはありませんが、 むしろ、『よく考えられたプログラム』をしっかり書くことがこの研究室の目標です。 ゆっくりしたペースで着実にものを考えられる人には居心地がよいことでしょう。


質問・見学

研究室見学はいつでも可能です。 なるべく事前に電子メイルで見学時間の相談をしてください。

亀山は総合研究棟B−1008にいますので、気軽に声をかけてください。E-mailは kam at cs.tsukuba.ac.jp です。
海野は、通常は総合研究棟B−1027にいます。E-mailは uhiro at cs.tsukuba.ac.jp です。(at を@に置き換えてください)。

今年の研究室紹介担当は、中尾(なかお、学類4年)です。 総合研究棟B−1027にいますので、気軽に声をかけてください。
E-mailは nakao at logic.cs.tsukuba.ac.jp です。(at を@に置き換えてください)。 また、その他の学生からも、各自の観点から率直な意見が聞けると思います。 (本当に自分にふさわしい研究室かどうかは、在籍する学生から直接取材して、 自分自身でしっかり判断してください。)


プログラム論理研究室ホームページ