当研究室では、型システムやプログラム解析、計算モデルなどの、プログラミング言語を設計・実装する上で必要となる基礎理論とそれらを実際の言語処理系に応用する研究をしています。型システムなどの基礎理論は、計算機言語論の講義でも述べた通り、近代的なプログラミング言語においては、プログラムを速く、安全に動作させるために極めて重要な役割を果たしてきています。当研究室では既存の型システムなどをさらに改良していくと同時に、近年の並列計算機やインターネットの普及に伴って新たに生じている並行・分散プログラムの安全性や効率の問題などを解決するための新しい種類の型システム・プログラム解析や計算モデルの研究をすすめています。具体的な研究内容については「最近の研究トピック」の項を参照して下さい。
以下では、研究室を選ぶうえでより参考になるように、研究内容のより詳しい説明、研究室での生活等について述べます。
卒業論文でこれらと関連するテーマを選ぶ必要は必ずしもありませんが、参考までに以下に最近の研究トピックを挙げておきます。これらの成果は進行中のものを除いて主要な国際会議や国際学術雑誌で発表しています。一部はここから見れます。
従来の逐次型言語の型システムでは、「整数を要求している関数を文字列に適用することがない」といった類のプログラムの安全性の保証をしていましたが、並行・分散プログラムの場合にはそれだけではプログラムが正しく動作するとはとても言えません。例えば、上のような誤りがなくても、デッドロックが起こってプログラムが止まってしまう可能性もあるし、非決定性のために結果が実行するたびに異なる、ということも起こり得ます。また、プログラムを効率良く動くコードに変換する上でも、従来の逐次型言語のコンパイル技術だけではうまくいきません。そこで、当研究室では（一部海外の研究者と協力して）、並行・分散プログラミング言語に適した新しい型システムの構築を行なってきました。現在も引続きその改良を行ない、実際に並行・分散プログラミング言語に適用するための準備を進めています。関連する論文および卒論・修論のテーマは以下の通りです。
他多数
プログラム実行中で使われなくなったメモリを回収・再利用するための手法としては、これまではガベージコレクションと呼ばれる、スタックやレジスタ等使われるとわかっている領域からポインタで順にメモリをたどっていき、たどられなかった領域を回収する方式が普通でした。この方式では、C言語のように malloc や free などを明示的にプログラマに書かせるのに比べて繁雑さがないし、誤って使っているデータを書き潰してしまうという誤りがないというメリットもあるのですが、一方ではプログラム固有の情報を用いているわけではないので、明示的に malloc, free を行なうようなC言語と比べてメモリの仕様効率が悪いことがあります。それに対し、最近になって、線形型システムやリージョン推論といった、プログラム中のメモリアクセスに関する解析を型システムを用いて静的に行なって、C言語の malloc や free に相当する操作を自動的に挿入するという手法が提案されました。そこで、当研究室でもそれらの手法の改良を行なってきました。関連する論文および卒論・修論のテーマは以下の通りです。
部分評価とは、入力の一部が他よりも早くわかる場合に、「先にできる計算は先にやってしまう」ことにより、プログラムの効率を drastic に向上させる方法です。たとえば一般に、何からのインタプリタにソースコードを与えて部分評価を行うと、コンパイラと同様の効果が得られることが知られています。最近では、普通の評価器を利用して効率的に部分評価を行う方法や、実行時に部分評価を行って動的に最適化を行う方法などが盛んに研究されています。当研究室でも、型を利用して効率的に部分評価を行う方法について研究し、その拡張や改良を提案してきました。関連する論文は以下の通りです。
最近になって、Javaというオブジェクト指向言語が流行していますが、MLなどの言語と異なり、言語仕様が自然言語で記述されていて曖昧であったり、あとから誤りが発見されたり、仕様と実装が食い違っていたりといったさまざまな問題があります。そこで、型つきλ計算を通してMLなど関数型言語を定義し、実装が議論されてきたのと同様に、Java のような言語の本質を表す計算系を用意してその動作や型システム等を形式的に記述し、正しさを検証しようという研究を博士課程の五十嵐君（現在留学中）が海外の研究者と共同で行なっています。関連する論文および卒論・修論のテーマは以下の通りです。
上のJava の問題でもあてはまりますが、プログラミング言語を設計するためには曖昧性のない、きっちりとした体系でそのプログラミング言語の仕様が決まっている必要があります。関数型言語等ではλ計算という形式的体系を用いればきっちりと言語の仕様を明確に定めることができたわけですが、並行・分散プログラミング言語のための形式的体系は確立されていませんでした。そこで、当研究室では並行・分散プログラミング言語の基礎となる体系として、線形論理に基づく計算モデルを構築し、それをもとに並行オブジェクトなどさまざまな言語機能の実現や上で述べた型システムの考案などの研究を行なってきました。関連する論文は以下の通りです。
他多数
従来まではプログラムの安全性の検査というと、ソース言語レベルで、型検査などを通じて行なうのが普通でした。ところが、最近になって、コンパイルされたコードをインターネットなどを介して取ってきて実行するといったことが日常茶飯事になってきて、それらの取ってきたコードが正しいかどうかの検査なども重要になってきました。そこで、Java の bytecode verification や Proof Carring Code や TAL といった抽象機械語やアセンブリ言語レベルでのコードの検証の研究が行なわれてきています。当研究室でも最近、そのような研究に着手しており、以下の卒業論文では、アセンブリ言語レベルで、プログラムの実行の停止性を検査する方法について研究をしてもらいました。
研究室に入ってからの研究生活はだいたい以下のようにすすみます。
４年生 … 卒業論文を書き上げるのが主な仕事です。が、いきなり卒業論文のテーマを決めて取り掛かれといわれてもほとんどの人は無理なので、最初の１、２カ月は各人の興味がある分野に応じて、研究の土台となる知識を獲得するために、関連する論文や教科書を読んでもらい、4年生同士で輪講をしてもらいます（小林研究室単独では数が少ないので、例年、米澤研の4年生と合同で行なっています。もちろんその輪講には私や大学院生の何人かが出席して適宜アドバイスや補足をします）。その後、11月ごろに卒論のテーマを決め、取りかかってもらいます。テーマは自分でやりたいテーマがあり、それが reasonable であると判断できればそれをやってもらいますし、そうでなければ、各人の興味に応じてこちらから提案したテーマの中から選んでもらいます。あとは適宜、研究室全体のミーティングあるいは個別のミーティングを通じて進行状況の報告、状況に応じた研究目標の修正をしつつ卒業論文をすすめてもらうことになります。
大学院進学後 … 修士課程での一大イベントは修士論文ですが、本格的に取り組むのは修士2年になってからの人が多いです。修士1年の間は、研究も進めてもらいますが、基本的には、研究者としての第一歩としてさまざまな経験を積んでもらうことになります。その中でも重要なのが、学会発表。卒業論文で行なった研究をまとめ、外の会議で論文発表をしてもらいます。この際、論文の書き方や論文の発表の仕方について本格的に指導を受けることになります。卒業論文で優れた結果をだせた人は海外で行なわれる国際会議で発表できる場合もあります（もちろん費用は研究室からでます）。その後も新しい成果がでれば適宜学会で発表してもらいます。また、米澤研究室と合同でセミナーを週１〜２回開いているので、そこで自分の研究や読んだ論文について発表したり、他の人の発表を聞いて議論をしながら、研究を発展させたり、新しい研究のアイデアを見つけると同時にそこでも発表技術を磨くことになります。さらに、それとは別に、小人数で非定期的に集まって特定の研究テーマに関する議論を行ないます。
皆さんにとってはプログラミング言語の研究といってもピンと来ないかもしれませんが、私（小林）は極めてやりがいのある分野だと思っています。プログラミング言語は（おそらくアルゴリズムと並んで）ソフトウェアの研究の王道だと言ってもいいすぎではないと思います。まず第一に、あらゆるソフトウェアがプログラミング言語を用いて記述されているわけですから、一つの言語処理系を改良するだけで、それを用いて書かれたプログラムすべてにその恩恵を与えることができます。第二に、プログラミング言語の研究は非常に幅広く、奥が深いということです。「どのようにしたらうまくソフトウェアを記述できるかとか」、「どのようにしたら記述したソフトウェアを高速に走る機械語に変換できるか」、といった工学的問題から、「このソフトウェアが正しく動作することをどのようにすれば証明できるか」、とか「そもそも計算とは何か？」、といった数学的な問題まで多岐にわたり、それらが密接に関係しています（例えば、プログラムの最適化を行なうこととプログラムの動作の解析・検証を行なうことには密接な関係があります）。それに応じて必要となる知識・能力も、アプリケーションプログラムやコンピュータのハードウェアに関する理解やプログラミングの経験から、高度な数学的能力までさまざまです。（かといってこれらすべてを身につけていないとだめかというとそうではなくて、むしろ逆でどれかに秀でていれば、それを生かして活躍できるような分野がプログラミング言語にはあるわけです）
当研究室の場合は、プログラミング言語の中でも、上の「最近の研究トピック」であげたような型システムやプログラム解析といった基礎理論を駆使して、それを改良して言語の設計や実装に役立てるという研究を中心に行なっています。これは、プログラミング言語の分野の中でも、いろいろな意味で一番おもしろくやりがいのある分野だと思っています。プログラミング言語の違った分野というと、抽象数学ののりで何のやくに立つのかわからない理論をつきつめるような研究や、ハッカー的なのりで実装をいろいろ工夫をしてこういつ場合にプログラムがこれだけ速くなりました、といった研究があります。ばりばりプログラムを書くのが好きな人は後者のような実装の研究も面白いとおもうかもしれませんが、このような研究はプログラムの経験が豊富でセンスさえあれば（情報科学科を卒業していなくても）ある程度だれにでもできることだし、現実的には、計算機言語論の講義でも述べた通り、最近の言語の実装技術は型システムなどを用いた高度なものになっており、単純な実装の工夫だけではやれることに限りがあります。型理論などをふまえないで言語の設計や実装をあれこれ工夫するのとそれらを駆使して行なうのとの差は、ちょうど、小学校の方程式などを使わない算数と、中学校以降の数学との違いに似たものがあると思います。方程式や微積分といった「道具」は最初は難しく感じるかもしれませんが、ひとたび理解してしまえば非常に便利で、かつそれらを使えば明快に問題を解くことができます。型システムなどの基礎理論もそれと同じです。
研究室を志望する人は、数学的なセンスがあるにこしたことはないですが、何よりも、とにかく研究に対して意欲のある人ならだれでも来てもらいたいです。自己満足できればいいというのでなく、国際的に認知されるような研究をしたい、という気概のある人なら誰でも歓迎しますし、そういう研究ができるように指導・環境作りをしていくつもりです。
E-mail: koba@is.s.u-tokyo.ac.jp
Jul. 2, 1999