Lambda LaboratoryInstitute of Science Tokyo の研究室サイト
言語:

研究

Lambda Laboratoryの研究テーマを紹介します。

ファーストクラス環境と環境計算

通常のプログラミング言語では、変数と値の対応を表す「環境」は処理系の内部に隠されています。この研究では、環境そのものをプログラム中の値として生成・受け渡し・合成できる「ファーストクラス環境」を理論化しました。ラムダ計算を拡張して、変数参照、環境の更新、関数適用を明確な簡約規則で表し、型安全性、型推論、合流性、評価戦略などを研究しています。動的なソフトウェア更新、モジュール、レコード、明示的代入などを統一的に理解する基礎にもなります。

関連研究

継続、線形論理、オブジェクト計算

「継続」は、ある時点から先に実行される計算を値として表したものです。例外処理、コルーチン、非局所脱出、バックトラックなどを統一的に記述できます。本研究では、継続をファーストクラスの値として扱うラムダ計算やオブジェクト計算を設計し、線形論理との対応、評価順序、型推論、制御効果を調べています。特に、資源を一度だけ使うという線形性と、計算を複製できる継続との関係を明確にし、高度な制御機構を安全に扱う型システムの基礎を与えています。

関連研究

型システム、意味論、プログラム解析

プログラムが期待どおりに動くことを、実行前に数学的に確かめる研究です。型システムは、単なるデータ型の検査だけでなく、関数の利用方法、制御の流れ、実行時に満たすべき条件まで表現できます。本研究では、多相型、線形型、漸進的型付け、詳細化型、効果システムなどを用いて、プログラムの安全性や性質を静的に保証する方法を検討しています。また、大ステップ意味論と小ステップ意味論、抽象機械、プログラム変換の関係を明らかにし、理論と実装を結び付けています。

関連研究

モデル検査による安全性、信頼性、DoS耐性の解析

モデル検査は、システムの状態を網羅的に探索し、望ましくない動作が起きないかを自動的に調べる技術です。本研究では、通信プロトコル、Webサーバ、メールシステム、負荷分散器などを形式モデルとして表し、安全性、信頼性、規則遵守、リアルタイム性を検証しています。特に、サービス不能攻撃に対する耐性を、時間や計算コストを含むプロセス代数として記述し、攻撃者とサーバの処理量の差を定量的に分析します。形式手法を実際のネットワークシステム設計へ応用する研究です。

関連研究

知的システム、分散計算、情報工学教育への応用

計算機科学の理論を、知的システムや教育、実用的なソフトウェアへ展開する研究です。人工知能では、知識表現と数値計算を組み合わせ、生命現象の複雑な制御を説明可能な形でシミュレーションしました。分散計算では、ブログなど既存のWeb基盤を計算資源として利用する方式や、オンライン証明・判定システムを研究しています。また、利用者の課題を出発点とするPBL型教育を通じ、要求分析、チーム形成、国際協働、システム開発を一体的に学ぶ情報工学教育を実践しています。

関連研究