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

概要

• 学生の自主性がモットーです。

  研究の基本は人です。個人個人の発想を大事にすること、 学生の目線で一緒に考えること、が研究室運営の基本だと考えています。もちろん、 この方針がうまくいくためには、学生側も自分の考え、 自分のやりたい研究がなにかしっかり考える必要があります。 自分がやりたい研究テーマをどんどん提案してください。

• 「ソフトウェア」と「論理」がキーワードです。

  ソフトウェア科学は、ソフトウェアの作り方に関する学問です。 本研究室では、ソフトウェアをがりがりたくさん書く人にも向いていますが、 もっと向いているのは、 自分の書いたソフトウェアがきちんと動くかが「気になる」人です。 どんなに高性能、高機能なソフトウェアも正しくなければ意味がありません。 でも、現実に世の中に流布しているソフトウェアはバグだらけです。 そんなソフトウェアを作り続けているのが馬鹿らしくなった人は、 是非本研究室に来て、 正しさの保証されたソフトウェアをつくる方法を一緒に考えてください。 そこでは、｢プログラムのための論理」が主役になります。

• 「異なる文化」を大事にし、積極的に交流をはかる人を育てたいと思っています。

  研究は、一人で黙々とやる段階も必要ですが、 異なるバックグラウンドや価値観を持つ人と交流して議論をすることも 非常に大事な要素です。 研究室の中だけで、あるいは、教員に与えられた題材だけで良い研究ができる とは限りません。積極的に外に出て、 自分の力でいろいろなことを発見してください。 このために、（１）学生には、研究室の中にこもらず、 外部の研究会等に参加・発表することを奨励しています。 （２）研究室の構成員として、出身の異なる学生（留学生や筑波大学以外の卒業生など）を 積極的に受け入れています。

研究内容

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

1. プログラム言語論（職人芸プログラミングを科学的なプログラミングへ）
   • ラムダ計算と型システムに基づくプログラム言語の体系 今日の先進的なプログラム言語（たとえば、ML や Ruby) の中核には、 関数と型システムがあります。これらの性質を研究することにより、 プログラム言語の本質が見えてきます。 また、型システムと論理の関係を解明することにより、 プログラム合成の基礎が得られます。 そこで、ラムダ計算（関数）と型に基づいたプログラム言語の研究を行っています。
     • 研究テーマの例： 「制御機構（コントロール機構)に関する型システム」、 「精密な制御機構をもつ型つきプログラム言語の設計」、 「環境を扱うプログラム言語の設計」、「並列計算・モバイル計算への応用」など。
   • プログラム変換とメタプログラミング(マルチステージプログラミング) メタプログラムとは、 「プログラムを入力として受け取ったり、生成したプログラムを返したりするプログラム」のことです。 このようなメタプログラムは、実際には、いたるところで使われていますが（例：webアプリケーション）, その正しさを一般的に保証する仕組みはまだあまり研究されていません。そこで、 メタプログラムの一種として、いくつかのプログラム変換を取り上げ、効率的で正しい変換について研究しています。
     • 研究テーマの例： 「部分計算（プログラム特化）の方法によるプログラム変換」、 「効率的なＣＰＳ変換（コンパイラで使われる変換）」、 「部分計算システムの実装・構築」
2. ソフトウェアの検証（プログラムや設計書に究極の保証を与える）
   • モデル検査による検証 モデル検査は、有限状態のシステム(ソフトウェア、ハードウェア、そのほか）が, 仕様（そのシステムが満たすべき性質）を満たすことを網羅的な探索により示す手法であり、近年の 計算パワーの上昇により, 非常に広い範囲のシステムの検証に用いられている「ホット」な話題です。 非常に状態数の多いシステムへの対処、 無限状態システムへの対処、実時間の記述、等々の拡張が待たれています。
     • 研究テーマの例： 「モデル検査による並列アルゴリズムの検証」、 「効率的な実時間モデル検査の研究」、 「モデル検査システムや定理証明システムのユーザインターフェースの作成」 など。
   • プログラム論理の体系と定理証明

     モデル検査は高速に処理ができる方法ですが、処理しきれない精密な仕様も存在します。 そのような場合、数学的な定理を証明するような形で、コンピュータ上でソフトウェアの性質を検証するのが 「定理証明』の手法です。 ここでは、様々なプログラム言語や論理体系を統一して記述し、 共通する性質を記述したり推論するための論理体系を構築し、 その上で、自動または手動で定理証明が可能な範囲を見つけだすことを目的として研究を行っています。

     • 研究テーマの例： 「論理フレームワークによるプログラム変換の定式化」、 「時相論理（モデル検査で使う論理）における自動的な定理証明」

学生に望む態度

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

セミナー

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

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

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

知っておくと良い科目

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

また、研究の材料を発掘するためには、情報学全般にわたって好奇心をもって接する態度が望まれます。

• 主専攻実験「関数プログラミング」、
• 専門科目: 「オートマトンと形式言語」、「プログラム言語論I」
• 専門基礎科目: 「論理と形式化」

文献

まず最初に読むとすると以下のいずれかが良いでしょう。

• 五十嵐淳、「プログラミング言語の基礎概念」、サイエンス社
• 萩谷昌巳、「ソフトウェア科学のための論理学」、岩波書店
• 小野寛晰、「情報科学における論理」、日本評論社

研究室生活について

• 研究室は総合研究棟Ｂ−１０２７号室（１０階）です。
• 研究室内は禁煙です。
• 私は時間を（自分の時間も他人の時間も）無駄にするのが嫌いですから、 無駄に学生を拘束することはありません。もちろん、どうしてもここをいま理解してもらいたい、 というときに話に熱中してしまうことはありますが、 基本的に定例セミナー以外の時間帯は自由に使ってください。 （もちろん、セミナー以外の時間に勉強しなくて良いという意味ではありません。 「毎日研究室にいなければいけない、といった拘束をしない」という意味です。 朝型でも夜型でも好きな時間に勉強して研究成果を出してください、という意味です。 言い換えれば、フレックスタイムということですね。）
• コンピュータの管理業務など研究室にとって必要な仕事も、 ある程度分担してもらわないといけません。新しいソフトをのせたり、 ネットワークを管理したりする業務はある程度はあります。 しかし、システム管理ばかりやって勉強の時間がなくならないよう、適当な量に留めるようにします。

進路

これまでの在籍者の進路は、 (学類卒業後に大学院に進学した後)、 情報系の企業を中心に、 関連業界に幅広く就職しています。 (NTT、NEC, 大日本印刷、三菱電機、楽天、Yahoo! Japan, カプコン、 ドワンゴ etc.)

研究設備

学生１人１台のノートPCとワーキングスペース (広い机/椅子)を確保します。

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

備考

基礎理論について:

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

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

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

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

質問･見学

研究室見学をしたい人は、教員あてにメイ ル等で見学時間の相談をしてください。

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

• 今年の研究室紹介担当は、B4の夏井と新田です。

  E-mailは haizoku at logic.cs.tsukuba.ac.jp です。(at を@に置き換えてください）。

また、その他の学生からも、各自の観点から率直な意見が聞けると思います。 （本当に自分にふさわしい研究室かどうかは、在籍する学生から直接取材して、 自分自身でしっかり判断してください。）

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