研究内容

• 2023年度振り返り
• 2022年度振り返り
• 2021年度振り返り
• 2020年度振り返り

• 限定継続演算子の理論と実装
• 定理証明系を使った各種性質の証明
• 証明木の可視化
• 初心者プログラミング教育（OCaml Blockly、型デバッガ、ステッパ）
• ゲーム開発用 universe ライブラリ
• OCaml Blockly を使った中高の学習教材開発

参考となる論文

限定継続 (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 節のみを理解すれば，まずはＯＫ。(応用は 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）に ついての論文。
      ４章で純粋な関数型に対する型システムの健全性を，
  ６章で call/cc が入った体系を
      扱っている。