Programming Logic Group
プログラム論理研究室
修士論文
２０１０年度
- "Type Inference for Effectful Multi-Stage Languages"
(エフェクトを持つマルチステージ言語の型推論）
小鍛治 雄一郎.
- "Identifying the Location of Type Error"
(型エラーの発生箇所の特定)
Cynthia Kustanto.
- "Orchid: A programming Language with Type-Safe Code Generation
for Web Applications"
(Orchid: Webアプリケーションのための型安全なコード生成機能を持つプログラミング言語)
高橋 宏文.
２００９年度
- "Multi-Stage Programming with Control Effect"
(計算エフェクトを持つマルチステージプログラミング),
杉浦 啓介.
- "Scalable Web Application Framework based on Delimited Continuation"
(限定継続に基づくスケーラブルなウェブアプリケーション構築手法), 田中 麻峰.
２００７年度
- "Dynamic Delimited Continuations with Polymorphism"
(多相性をもつ動的限定継続), 米澤 拓央.
２００６年度
- 「階層化コントロールオペレータに対する型システムの構築とその性質に関する研究」、
鈴木 輝信.
- 「動的環境と限定継続をもつプログラム言語の意味論と実装」、田中 陽.
- 「オブジェクト指向言語に対するメタプログラム言語の設計と実装」、佐々木 卓.
２００５年度
- 「多値モデル検査によるモデルの冗長性の削減」、辰巳 淳朗.
- 「プログラムに対する変換の正しさの形式検証」、吉原 宏之.
２００４年度
- 「効率良い実時間モデル検査を実現する遷移除去と抽象化・精密化技法の提案」、中島 一.
卒業論文
２０１０年度
- 「限定継続コントロールオペレータの実装方式の調査と比較」、
宮部浩太朗．
- 「証明支援系Coqを用いた計算体系が持つ性質の形式的手法による証明」、
渡邉公隆．
２００９年度
- 「複数のプロンプトをもつ限定継続機構に対するＣＰＳ変換と抽象機械の構築」、 高島尚希．
- 「多値有界モデル検査における論理式変換アルゴリズムの改善の提案」、金鎭慶．
２００８年度
- 「ステージ化によるドメイン特化言語処理系の安全な高速化」, 小鍛冶 雄一郎.
- 「充足可能性問題を効率よく解決するためのアルゴリズムの実装と検証」, 棚町 雅史.
- 「モデル検査器BLASTによる C言語プログラムの検証」, 舘石 直人.
２００７年度
- 「マルチステージプログラミングのための計算体系の実装」、杉浦啓介.
２００６年度
- 「Formulation of Dependently Typed Context Calculus
(依存型つき文脈計算の定式化）」、畑山 大輔.
- 「低レベル言語に対するモジュラーな検証のための型システム」、安岡 宏俊.
-
２００５年度
- 「動的階層化モナドの設計と実装」、米澤 拓央.
- 「状態数削減法による鉄道信号制御システムに対するモデル検査の実装と評価」、チョサンクン.
２００４年度
- 「オブジェクト指向言語における潜在的危険性を含む型変換の静的検査」、佐々木 卓.
- 「参照型とcall/ccに対応した多相的な型推論システム」、鈴木 輝信.
２００２年度
- 「分散アルゴリズムに対するモデル検査による検証」、中島 一.