階層的コントロールの論理とプログラム抽出

• 研究課題/領域番号: 23650003
• 研究種目: 挑戦的萌芽研究
• 配分区分: 基金
• 研究分野: 情報学基礎
• 研究機関: 筑波大学
• 研究代表者: 亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
• 研究期間 (年度): 2011 – 2012
• 研究課題ステータス: 完了 (2012年度)
• 配分額: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円); 2012年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2011年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
• キーワード: プログラム理論 / ソフトウェア基礎論 / プログラム言語 / 型システム / コントロール・オペレータ / プログラム抽出 / コントロールオペレータ / 限定継続 / Curry-Howardの対応 / ラムダ計算 / CPS変換

研究概要

プログラムの実行順序を制御するコントロールオペレータについて、必要呼び計算と並列計算の2つの設定で、論理的な側面の研究を行った。前者においては、論理型プログラミング言語のある種の探索機能と関数型プログラミング言語の限定継続コントロールオペレータが対応することを示した。後者においては、適切なコントロールのもとで、コントロールオペレータを持つ並列計算体系が透過的な意味論を持つことを証明した。

研究成果

• [雑誌論文] 限定継続機構とfuture を持つ計算体系の透過的意味論 (2013)
  • 著者名/発表者名: 田中麻峰,亀山幸義
  • 雑誌名: 情報処理学会論文誌
  • NAID: 110009596040
  • 査読あり
• [雑誌論文] Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras (2012)
  • 著者名/発表者名: Jefferson O. Andrade, Yukiyoshi Kameyama
  • 雑誌名: Special Section on Formal Approach, IEICE Transactions on Information and Systems 巻: 5 ページ: 1335-1364
  • NAID: 10030942823
  • 査読あり
• [雑誌論文] Efficient Multi-Valued Bounded Model Checking for LTL over Quasi-Boolean Algebras (2012)
  • 著者名/発表者名: Jefferson O. Andrade, Yukiyoshi Kameyama
  • 雑誌名: IEICE Transactions on Information and Systems 巻: Vol. E95-D, No. 5 ページ: 1355-1364
  • NAID: 10030942823
  • 査読あり
• [雑誌論文] Type checking and typability in domain-free lambda calculi (2011)
  • 著者名/発表者名: K.Nakazawa, M.Tatsuta, Y.Kameyama, H.Nakano
  • 雑誌名: Theoretical Computer Science 巻: 412(44) 号: 44 ページ: 6193-6207
  • DOI: 10.1016/j.tcs.2011.06.020
  • 査読あり
• [学会発表] Lazy Delimited Nondeterminism (2012)
  • 著者名/発表者名: Sebastian Fischer, Michael Hanus, Yukiyoshi Kameyama, Chung-chieh Shan, Naoki Takashima
  • 学会等名: International Workshop on Functional and (Constraint) Logic Programming (WFLP 2012), Work-in-Progress session
  • 発表場所: 名古屋大学
  • 年月日: 2012-05-29
• [学会発表] Lazy Delimited Nondeterminism (2012)
  • 著者名/発表者名: Sebastian Fischer, Michael Hanus, Yukiyoshi Kameyama, Chung-chieh Shan, Naoki Takashima
  • 学会等名: International Workshop on Function and Constraint Logic Programming (WFLP 2012)
  • 発表場所: 名古屋大学
• [学会発表] コントロールオペレータを持つ必要呼び計算体系の設計 (2011)
  • 著者名/発表者名: 西山達也, 亀山幸義
  • 学会等名: 情報処理学会第86回プログラミング研究会(PRO86)
  • 発表場所: 神奈川近代文学館(横浜市)
  • 年月日: 2011-11-02
• [学会発表] Efficient Algorithms for Analyzing Verification Errors (2011)
  • 著者名/発表者名: Jin-gyeong Kim, Yukiyoshi Kameyama
  • 学会等名: 日本ソフトウェア科学会ディペンダブルシステムワークショップ＆シンポジウム
  • 発表場所: 京都工芸繊維大学・京都府