バグのないソフトウェア構築環境に関する研究の新展開

2010 Fiscal Year Annual Research Report

• Project/Area Number: 22300008
• Research Institution: Kyoto University
• Principal Investigator: 佐藤 雅彦 京都大学, 情報学研究科, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 五十嵐 淳 京都大学, 情報学研究科, 准教授 (40323456) ; 中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581) ; 山本 章博 京都大学, 情報学研究科, 教授 (30230535) ; 湯淺 太一 京都大学, 情報学研究科, 教授 (60158326)
• Keywords: 自然枠組 / ソフトウェア開発 / ソフトウェア検証 / メタ言語 / メタ理論 / 式の理論 / 抽象操作

Research Abstract

本研究では,プログラムの正しさを保証するための検証システム,および,その検証自体の正しさを保証するメタ理論に関する議論をともに行うことのできるフレームワークの実装に向けて,自然枠組(Natural Framework,NF)の設計と構築を行っている.本年度は,NFを実装するためのプログラミング言語の仕様の詳細化を行った.より具体的には以下のとおりである.
この言語の中核部分で必要となる数学的対象は,それぞれ,ある基本的な「概念」(concept)を満足するものとして特徴づけられるという重要な性質をもつ.すなわち,個々の対象は,対象それ自体でなく,それが満たす固有の概念とともに存在すると考えられる.このような対象を「第一種の数学的対象」と呼び,その対象の集りがつくる数学的構造について研究をした.
今後は,この設計をもとに言語の実装を行い,このプログラミング言語の上でNFを実現することが期待される.

Research Products

• [Journal Article] External and internal syntax of the λ-calculus (2010)
  • Author(s): Masahiko Sato, Randy Pollack
  • Journal Title: Journal of Symbolic Computation Volume: 45 Pages: 598-616
  • Peer Reviewed
• [Journal Article] Semantics of a graphical model for representing hypotheses and a system supporting management of hypotheses (2010)
  • Author(s): Ikeda, M., Nishino, M., Doi, K., Yamamoto, A., Hayashi, S.
  • Journal Title: Proceedings of the Fifth International Conference on Knowledge, Information and Creativity Support Systems, KICSS2010 Volume: LNAI 6746 Pages: 32-43
  • Peer Reviewed
• [Journal Article] A logical foundation for environment classifiers (2010)
  • Author(s): Takeshi Tsukada, Atsushi Igarashi
  • Journal Title: Logical Methods in Computer Science Volume: 6 Pages: 1-43
  • Peer Reviewed
• [Presentation] 多相型と存在型に対する型検査問題の同値性 (2011)
  • Author(s): 加藤祐輝, 中澤巧爾
  • Organizer: 第13回プログラミングおよびプログラミング言語ワークショップ(PPL2011)
  • Place of Presentation: 北海道札幌市
  • Year and Date: 2011-03-09