研究内容

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

参考となる論文

限定継続 (shift/reset) 関係
  • Danvy, O., and A. Filinski 著者のページ / ACM
    "Abstracting Control"
    Proceedings of the 1990 ACM Conference on
    Lisp and Functional Programming, pp. 151-160 (June 1990).
        shift/reset の論文と言えばこれ。
        少し難しいけど 1 節のみを理解すれば,まずはOK。(応用は 3 節)
  • Danvy, O., and A. Filinski 著者のページ
    "A Functional Abstraction of Typed Contexts"
    Technical Report 89/12, DIKU, University of Copenhagen (July 1989).
        shift/reset の単相の型システムが出ている論文。
CPS 変換関係
  • Danvy, O., and A. Filinski 著者のページ
    "Representing Control, a Study of the CPS Transformation"
    Mathematical Structures in Computer Science, Vol. 2, No. 4, pp. 361-391
    (December 1992).
        CPS 変換について書いてある論文。
        少し長いけど,その分,わかりやすい論文。
        この論文で CPS 変換の administrative redex の問題が解決している。
        また,shift/reset のインタプリタを shift/reset 自体を 使って書いたものも出ている。
対称 λ 計算関係
  • Filinski, A. 著者のページ
    "Declarative Continuations and Categorical Duality"
    Master's thesis, DIKU Report 89/11, University of Copenhagen (August 1989).
        Filinski の対称 λ 計算についての修士論文。
型関係
  • Wright, A. K., and M. Felleisen. 論文のあるページ
    "A Syntactic Approach to Type Soundness"
    Information and Computation, Vol. 115, No. 1, pp. 38-94 (November 1994).
        型システムの健全性(Progress と Preservation)に ついての論文。
        4章で純粋な関数型に対する型システムの健全性を,
    6章で call/cc が入った体系を
        扱っている。