限定継続の計算系と論理

2003 Fiscal Year Annual Research Report

• Project/Area Number: 13680411
• Research Institution: University of Tsukuba
• Principal Investigator: 亀山 幸義 筑波大学, 電子・情報工学系, 助教授 (10195000)
• Keywords: コントロール・オペレータ / ソフトウェアの検証 / 限定継続 / 公理化 / 関数型プログラム言語

Research Abstract

本研究の目的は、制御演算子(コントロール・オペレータ)を持つ計算系を型理論および論理の視点から観察することにより,その妥当な定式化や意味についての理論を展開すること、および、その理論に基づき,仕様を表す論理式が与えられた時,その仕様を満たす,制御演算子を持つ関数型プログラムを作成するという手法へ応用することである。前年度の本研究では、『限定継続』と呼ばれる制御演算子の健全かつ完全な公理化を行ったが(発表は本年度)、本年度はこれをさらに拡張して、『多レベルの限定継続』の計算体系について検討を行った。その結果、(1)限定継続演算子を持つプログラムを組み合わせて大きなソフトウェアを構成する場合において、前年度に扱った単純な限定継続では問題があること、(2)この問題は、多レベルの限定継続を使うと解消されること、(3)多レベルの限定継続に対する健全かつ完全な公理体系が前年度の公理体系の拡張として得られること、の3点の成果を得た。特に、健全かつ完全な公理については、レベル2やレベル3という個別の場合だけでなく、任意のレベルに対する公理化を完成したという意味で、本研究が当初目的としていた目標を完全に達成することができた。このほか、メタ変数の取り扱いについても従来の体系にはない代入(textual substitution)を持つ体系の定式化に成功し、この2つの成果を合わせることにより、部分計算やCPS変換など、プログラムをデータとして扱うプログラムの検証を行うことが可能になった。

Research Products

• [Publications] Yukiyoshi Kameyama, Masahito Hasegawa: "A Sound and Complete Axiomatization for Delimited Continuations"Proceedings of Eighth ACM International Conference on Functional Programming. 177-188 (2003)
• [Publications] Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, Atsushi Igarashi: "Calculi of Meta-variables"Proceedings of 17^<th> International Workshop on Computer Science Logic, Lecture Notes in Computer Science. 2803. 484-497 (2003)
• [Publications] Yukiyoshi Kameyama: "Axiomatizing Higher-Level Delimited Continuations"Proceedings of Fourth ACM-SIGPLAN Continuation Workshop. 49-53 (2004)
• [Publications] 亀山幸義, 中島一: "ケーススタディ:モデル検査と定理証明を用いた鉄道信号制御システムの検証"システム検証の科学技術シンポジウム予稿集. 82-91 (2004)