New development of research on bug-free software construction environment

• Project/Area Number: 22300008
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Kyoto University
• Principal Investigator: SATO Masahiko 京都大学, 大学院・情報学研究科, 名誉教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): YUASA Taiichi 京都大学, 大学院・情報学研究科, 名誉教授 (60158326) ; YAMAMOTO Akihiro 京都大学, 大学院・情報学研究科, 教授 (30230535) ; IGARASHI Atsushi 京都大学, 大学院・情報学研究科, 教授 (40323456) ; NAKAZAWA Koji 京都大学, 大学院・情報学研究科, 助教 (80362581)
• Project Period (FY): 2010 – 2012
• Project Status: Completed (Fiscal Year 2012)
• Budget Amount: ¥17,940,000 (Direct Cost: ¥13,800,000、Indirect Cost: ¥4,140,000); Fiscal Year 2012: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000); Fiscal Year 2011: ¥6,110,000 (Direct Cost: ¥4,700,000、Indirect Cost: ¥1,410,000); Fiscal Year 2010: ¥7,410,000 (Direct Cost: ¥5,700,000、Indirect Cost: ¥1,710,000)
• Keywords: ソフトウェア検証 / クラス理論 / ソフトウェアの安全性 / 型理論 / 項書換 / 自然枠組 / ソフトウェア開発 / メタ言語 / メタ理論 / 式の理論 / 抽象操作

Research Abstract

We started our research by setting the goal of realizing acomputer environment for developing bug-free softwares, so that we can guarantee thesafety of computer software. We have achieved the goal by implementing a prototypesystem. In particular, as a part of the system, we implemented a programming languagewhich can be used to reason about the properties of the system itself. The interfacebetween the user and the system is also implemented by this programming language.

Research Products

• [Journal Article] A Canonical LocalRepresentation of Binding (2012)
  • Author(s): Randy Pollack, Masahiko Sato andWilmer Ricciotti
  • Journal Title: Journal ofAutomated Reasoning Volume: Vol. 49 Pages: 185-207
  • Peer Reviewed
• [Journal Article] A Canonical Local Representation of Binding (2012)
  • Author(s): Randy Pollack
  • Journal Title: Journal of Automated Raesoning Volume: 49 Issue: 2 Pages: 185-207
  • DOI: 10.1007/s10817-011-9229-y
• [Journal Article] SATソルバーを用いた帰納論理プログラミング (2012)
  • Author(s): 近藤誠一, 山本章博
  • Journal Title: 第84回人工知能基本問題研究会資料 Volume: SIG-FPAI-B104-14 Pages: 75-80
  • Peer Reviewed
• [Journal Article] Constructive linear-time temporal logic:Proof systems and Kripke semantics (2011)
  • Author(s): Kensuke Kojima and Atsushi Igarashi
  • Journal Title: Information and Computation Volume: Vol.209(12) Pages: 1491-1503
  • Peer Reviewed
• [Journal Article] A Canonical Local Representation of Binding (2011)
  • Author(s): Randy Pollack, Masahiko Sato, Wilmer Ricciotti
  • Journal Title: a special issue of Journal of Automated Reasoning
  • Peer Reviewed
• [Journal Article] Type checking and typability in domain-free lambda calculi (2011)
  • Author(s): K.Nakazawa, M.Tatsuta, Y.Kameyama, H.Nakano
  • Journal Title: Theoretical Computer Science Volume: 412(44) Issue: 44 Pages: 6193-6207
  • DOI: 10.1016/j.tcs.2011.06.020
  • Peer Reviewed
• [Journal Article] External and internal syntax of thelambda-calculus (2010)
  • Author(s): Masahiko Sato, and Randy Pollack
  • Journal Title: Journal of SymbolicComputation Volume: Vol.45
  • Peer Reviewed
• [Journal Article] A logical foundation for environmentclassifiers (2010)
  • Author(s): Takeshi Tsukada and Atsushi Igarashi
  • Journal Title: Logical Methods in ComputerScience Volume: Vol.6(4:8) Pages: 1-43
  • Peer Reviewed
• [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] Viewing lambda-termsthrough maps (2013)
  • Author(s): 佐藤 雅彦
  • Organizer: 3rd Workshop on Proof Theory and Rewriting
  • Place of Presentation: 石川県立美術館 (金沢市)
  • Year and Date: 2013-03-07
• [Presentation] 整数計画ソルバを用いた帰納論理プログラミング (2013)
  • Author(s): 山本章博
  • Organizer: 人工知能学会第89回人工知能基本問題研究会(SIG-FPAI)
  • Place of Presentation: 岩手県立大学
• [Presentation] Essence of de BruijnIndex (2012)
  • Author(s): 佐 藤 雅 彦
  • Organizer: 37th TRS meeting
  • Place of Presentation: 岩沼屋 (仙台市)
  • Year and Date: 2012-11-07
• [Presentation] 多相型と存在型に対する型検査問題の同値性 (2011)
  • Author(s): 加藤祐輝, 中澤巧爾
  • Organizer: 第13回プログラミングおよびプログラミング言語ワークショップ(PPL2011)
  • Place of Presentation: 北海道札幌市
  • Year and Date: 2011-03-09
• [Presentation] Viewing lambda-terms through maps
  • Author(s): 佐藤 雅彦
  • Organizer: 3rd Workshop on Proof Theory and Rewriting
  • Place of Presentation: 石川県立美術館