本文へジャンプ

学科概要
  • HOME
  • 学科概要
  • 学生による学科紹介

学生による学科紹介

4年生になると「研究室」に配属されます。
今までは、皆で同じ授業を受け同じ問題を解いてきたのが各人で「自分は何をしよう」と考える初めての経験です。4年の前期に3研究室に仮配属、どの研究室に行こうかじっくり検討、4年の後期は本配属、卒業研究を行います。
そして、大学院に入ると、研究が生活の中心になっていきます。

小林研究室 | 小林直樹教授、松田一孝助教
短い説明
ソフトウェアおよびプログラミング言語に関する基礎理論と、その応用としてプログラム検証やプログラム変換、新しいプログラミング言語の設計などについて研究を行っています。最近は特にプログラムの自動検証の研究に力をいれています。

小林先生に聞きました
Q1) 小林研の研究の対象は何ですか

ソフトウェアとその基礎理論。基礎理論としては、計算モデルとプログラム意味論、型理論、形式言語とオートマトンなど。

Q2) プロジェクトがあれば紹介していただけますか

「高階モデル検査とその応用」。従来から研究されていたシステム検証手法として「モデル検査」というのがあり、発案者らが2007年のチューリング賞を受賞しています。「高階モデル検査」はそれを拡張・一般化したもので、原理的に可能であることが示されたのが2006年という、ごく新しいシステム検証手法です。2009年に当研究室で現実的な時間で動作するアルゴリズムを世界に先駆けて考案しました。現在、これをさらに改良するとともに、プログラム検証やデータ圧縮などへの応用について研究しています。

Q3) 小林研の特徴は何だと思われますか

理論と実践の両立を目指しているところでしょうか。ソフトウェアに関する理論というのは、数学や論理学などとも結びついて奥が深く、知的興味をそそられて面白いです。しかしそれだけでは自己満足になりがちですので、プログラム検証など、具体的な応用を見据えて研究を進めるのが大事だと思っています。一方で、目先の応用ばかりに目をとられると、小手先の技術に走りがちになり、世の中に革新をもたらすような大きな成果は生まれません。そこで、理論の学術的奥深さとその実社会への応用(といっても数十年後という長期的視野に立ったものですが)を両立すべく研究をしています。上で挙げた高階モデル検査はまさにその具体例の一つで、プログラムの自動検証やデータ圧縮という重要な応用を見据えると同時に、計算モデル(λ計算など)、型理論、形式言語理論、計算量理論など、理論計算機科学の様々な理論を総動員して研究を進めています。

Q4) どのような学生に研究室に来てほしいですか

上で書いた理論と実践の両立に共感し、研究を通して世の中にインパクトを与えようという意欲・野心のある人。

Q5) どのような知識が必要でしょうか

学部レベルのコンピュータサイエンスの素養をきちんと身につけていれば十分で,その他の必要知識は研究室に入ってから学べばよいと思います。
松田助教に聞きました
Q1) 小林研の研究の対象は何ですか

プログラミング言語の基礎理論やその応用についてです.

私は,中でも,プログラム変換や領域特化言語,関数プログミング技術について研究しています.

Q2) プロジェクトがあれば紹介していただけますか

現在,小林研では「高階モデル検査」とその応用についての研究が集中的に行われています.

Q3) 小林先生はどのような方と思いますか

物事に対して常に真剣で,自分にも(他人にも)厳しい方だという印象をもっています.

あと,研究室の外から見るとわかりづらい点としては,とても面倒見がよい方だと思います.
少なくとも小林研では「研究室に入ったはいいが放置される」ってことはないかと.

時間の使い方もうまく,あれだけミーティングや議論の時間を重視しているのに,
自分の研究が進められるというのは見習いたいところです.

Q4) 小林研の特徴は何だと思われますか

「研究をやろう」,特に「世界的に評価されるような研究をやろう」
という空気がしっかりできているところにあると思います.
学生も含めて,みんなが真剣に研究に取り組んでいるので,毎週のゼミはとても刺激的です.

また,今(2013年6月)は,教員二人のほかに博士研究員が三人と,
プロフェッショナルな研究者が五人所属していて,
研究および研究生活を進める上で議論・相談の相手にことかかないので,
研究環境としては充実したものになっていると思います.

Q5) どのような学生に研究室に来てほしいですか

あくまで私個人の意見ですが,「生意気だ」と感じるくらい元気な学生に来てほしく思います.

Q6) どのような知識が必要でしょうか

やる気さえあれば,研究室に入ってから必要なことを学べばそれでよいと思います.

Q7) 演習三の課題を教えていただけますか

それぞれの学生が興味のある研究テーマに対し,
教科書や最近の論文を読んだり,論文のアイデアを実装したりという感じです.
竹井さん(修士課程二年)に聞きました
Q1) 竹井さんの研究の対象はなんでしょうか

人間がソフトウェアを作る際には、プログラムの誤りが生じてしまうことが多々あります。そのような欠陥がないかを自動的に検査する際、対象となるソフトウェアの実行中の状態を把握する必要があります。私の研究では、そのような状態モデルの作成手法を対象として、数理的な方法で改善することを試みています。

Q2) 小林研の特徴は何だと思われますか

学生ごとに個別の週例ミーティングがあり、とても建設的な指導を受けられます。私の場合、先生からいただける提案によって、問題解決の新たな手法を組み立てることができ、そのたびに少しずつ前進しています。

また、いくつかのデモ プロジェクトがあり、組み立てた理論をそれらに組み込んで実践することが多いので、プログラミングの機会
(特に関数型言語で) が多いかもしれません。

Q3) 小林先生はどのような方と思いますか

さまざまな面で、とても効率が良い方だと思います。無駄な時間を使うことを非常に嫌われるようです。

チョコレートとナッツがお好きです。

Q4) 小林研にきて、どのような点が良かったでしょうか

私はもともとプログラムを組むのが好きで情報科学を志した人間なのですが、その道具たるプログラミング言語についてメタな研究をできることがとても興味深いです。

また、週例ミーティングが良いプレッシャーとなり、自分自身の効率を意識するようになりました。なにより、世界の他のチームも同類の問題を解こうと鎬を削っていることを肌で感じられますので、大学院生として研究のイロハを学ぶには良い環境だと思います。
桑原さん(修士課程一年)に聞きました
Q1) 桑原さんの研究の対象はなんでしょうか
高階関数型プログラムの停止性を自動で検証する手法について研究しています。

Q2) 小林研の特徴は何だと思われますか
まず扱っている分野については、
かなり抽象度の高い、いわば「数学」色が強い議論で研究が進んでいくにもかかわらず、
言語の性質やプログラムの検証など、研究成果が「コンピュータ科学」としての性質を色濃く持っているのが特徴だと思っていて、
数学的・論理学的な理論が実際にプログラミングの技術として応用されていくのを実感できる研究室だと思っています。

あとは研究室の雰囲気ですが、
毎日のように研究室の中央にあるホワイトボードで研究室のメンバーで議論が交されていたりと、
まだ人は少ないながらもそういった「研究に対する熱意」を持った人間が集まっていることが感じられる環境です。

Q3) 小林先生はどのような方と思いますか
かなり仕事熱心な性格を持っている方だと感じています。
またとても面倒見がいい方で、卒業研究のときには細かく指導していただきました。

Q4) 小林研にきて、どのような点が良かったでしょうか
自分は型や関数型言語といったテーマが好きなので、
そういった分野の最前線の研究に触れられる環境に来られたという点が良かったと思っています。

また、週一回の打ち合せ・ゼミでの進捗報告があったり、
加えて研究室のゼミでは定期的に各メンバーに発表順が回ってきたりもするので、
適度に緊張感があって研究のペースを作りやすい環境であるという点も自分には大きなプラスでした。