大堀・上野研の研究内容

大堀・上野研究室では,プログラミング言語やデータベースの研究を中心に,高機能で安全な新しいソフトウェア構成基盤の実現を目指した研究に取り組んでいます.さらに,これらの研究の成果を装備した次世代高信頼プログラミング言語SML#の開発を推進しています.

本ページでは,大堀・上野研究室の研究概要を紹介します.より専門的な内容は,主要な発表論文や,大堀・上野研メンバー及び共同研究者から辿れる各スタッフのWebページを参照ください.

研究領域:プログラミング言語とデータベース

現代社会は多様で膨大なソフトウェア群によって支えられています.これらのソフトウェア基盤は,一度完成し稼働し始めればあとは放っておいてもよい,というものではありません.社会のニーズはますます複雑・多様化し,コンピューティング環境やインターネットも常に進化を続けています.その変化に合わせて,より高度で,より複雑なソフトウェアが次々と生産されなければなりません.

その一方で,ソフトウェアは高機能であるだけでなく,信頼できるものでなければなりません.社会の基盤がソフトウェアで支えられている以上,ソフトウェアの信頼性は社会そのものの信頼性に直結します.人間の要求がどんなに高まり,ソフトウェアがどんなに複雑になろうとも,ソフトウェアは人間の期待通りに動き続けなければなりません.

このような社会が信頼性・利便性を確保しながら発展してゆくためには,これまでよりも高機能で複雑なソフトウェアを,高い生産性と信頼性を保ったまま,開発できるようなプログラミング環境が必要です.その実現に向けて,当研究室では,ソフトウェアを形作るための最も根幹にある技術要素であるプログラミング言語とデータベースに着目し,これらを人類が自由自在に,かつ高い信頼性を寄せて使いこなせるようになることを,ソフトウェア開発における究極の課題であると考えています.

この究極の目標の達成に向けて,当研究室では,

  • 基礎:プログラミング言語の信頼性を支える基礎理論の整備
  • 実装:高い記述性と信頼性を両立するコンパイラの開発技術の確立
  • 応用:ソフトウェア開発における最新のニーズを実現するプログラミング言語機能の開発

など,プログラミング言語の基礎理論やその実装技術の研究に取り組んでいます.

さらに,これら研究の具体的な成果として,我々の目指す次世代プログラミング環境を自ら作り出すことを目指し,

  • 次世代関数型言語SML#の開発
  • SML#の産業的応用に向けた産学連携研究

などにも力を入れています.

プログラミングに関する原理,基礎理論,実装技術の探究から,実用規模の言語とコンパイラの実現,その産業的応用に至るまで,多岐にわたるテーマに一貫して取り組んでいるのが,当研究室の大きな特徴です.この体制のもと開発されたSML#コンパイラは,国内外で高く評価され,学術界だけでなく産業界でも注目を集めています.

プログラミング言語の基礎理論の研究

数学を典型とする近代の自然科学が,種々の抽象概念を組織的かつ階層的に導入することを可能にする記述システムを持つことによって急速な発展を遂げたように,情報科学が,複雑なソフトウェアを信頼性を持って効率よく開発する体系を確立し発展させていくためには,プログラミングで有用な種々の抽象化や構造化を導入する記述システムが必要です.この記述システムがプログラミング言語です.

当研究室では,数理論理学,型理論,ラムダ計算,形式言語理論など,論理学や数学によって洗練された種々の概念を用いながら,最先端のハードウェアやネットワーク環境を生かす,より高水準で効率よいプログラミング言語の開発の基礎となる基本原理やコンパイルの理論に関する研究を行っています.例えば,以下のような研究テーマに取り組んでいます.

  • Curry-Howard同型関係の考え方に基づく系統的なコンパイルやコード検証
  • 型情報をコンパイルに必要な情報と考えることにより,高度な言語機能を効率的なコードに変換する型主導コンパイル方式
  • 関係データベース問い合わせ言語SQLの型付き関数型言語への統合
  • 実用プログラミング言語の操作的意味論に関する研究

当研究室では,これらの分野での先駆けとなる成果をあげ,現在も最先端の研究を推進しています.

プログラミング言語の実装技術の研究

基礎研究により達成された高い記述力や信頼性も,現実のプログラミング環境として実現されなければ,現場のソフトウェア開発には届きません.また,たとえプログラミング環境が整備されたとしても,今実際に存在するハードウェア資源やソフトウェア資源をフル活用できるようなコンパイラがなければ,そのような言語はやはり使い物になりません.

当研究室では,関数型言語を次世代プログラミング環境の核となる技術と考え,従来の関数型言語の欠点を解消し,関数型言語に他の実用言語と比類ない実用言語とするための基礎理論および実装技術を開発しています.例えば以下のようなテーマに取り組んでいます.

  • メモリ上で自然なデータ表現を実現するコンパイル方式
  • オブジェクトを移動しない高効率な並行ゴミ集め(garbage collection)方式
  • シームレスなコールバックを含む,C言語との高度な連携を実現する言語間インターフェース
  • 外部データを型付き言語から取り扱うための部分動的レコードの理論と実装
  • 関数型言語への自然結合演算の導入

SML#コンパイラの開発

これらの研究成果を全て装備した世界最先端の高信頼プログラミング環境の実現を目指し,次世代プログラミング言語SML#およびそれを中核とする次世代プログラミング環境を開発しています.SML#については以下のページをご覧ください.

関連ページ