研究内容

主な研究内容
  • 継続計算に対する仮想機械の導出
  • 定理証明系Coqを使った各種継続計算の性質の証明
  • 対称 λ 計算
  • shift/resetを含む部分評価器の実装
  • MinCamlコンパイラ,Caml Lightにおけるshift/resetの実装
  • 証明木(ほか)の可視化
  • お茶大情報科学科の時間割自動作成

2008年度のゼミ

  • 『四則演算インタプリタを作ろう!』
    1. 四則演算インタープリタをつくりましょう
    2. 末尾呼び出し(tail call)と継続渡し形式(Continuation Passing Style)
    3. lexer(字句解析器)と parser(構文解析器)の作成  (サンプルコード)
    4. 局所変数の導入
    5. 関数(closure)の追加
    6. 大域脱出(exit)の追加
    7. 再帰関数の追加
    8. FelleisenのCオペレータ
    9. リストの追加
    10. Promptの導入
    11. control/prompt から shift/reset への拡張
  • 対称 λ 計算
  • Coq ゼミ
    1. Coq のインストール,関数,大域的変数, Specification の定義
    2. 命題論理
    3. 関数の拡張,述語論理
    4. implication (ならば,→) 以外の論理演算,等式の証明
    5. 帰納的なデータ型 (再帰を含まないもの/含むもの) ,再帰関数の定義,帰納法
    6. リスト,帰納的な命題の定義
    7. 演習
    8. 演習(続き)
  • Hanne Riis Nielson, Flemming Nielson ( 本のページ / Hanne Riis Nielson のページ / Flemming Nielson のページ)
        "Semantics with Applications: A Formal Introduction"
    1. 1 章途中 (p.13) までの資料 (PDF 版)
    2. 1 章最後までの資料 (PDF 版)
    3. 2 章途中までの資料 (PDF 版)
    4. 2.2 節最後までの資料 (PDF 版)
    5. 2.3 節の資料 (PDF 版)
    6. 2.4 節の資料 (PDF 版)
    7. 2.5 節の資料(1) (PDF 版)
    8. 2.5 節の資料(2) (PDF 版)
    9. 3 章の資料 (PDF)
    10. 4 章の資料 (PDF)

  • Coq ( 見るページ )

  • ※参考となる論文