依存型理論による安全性保証付きデータ構造の創出・推論・進化

• 研究課題/領域番号: 24300001
• 研究種目: 基盤研究(B)
• 配分区分: 一部基金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 群馬大学
• 研究代表者: 浜名 誠 群馬大学, 大学院理工学府, 助教 (90334135)
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 6,370千円 (直接経費: 4,900千円、間接経費: 1,470千円); 2014年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2013年度: 1,950千円 (直接経費: 1,500千円、間接経費: 450千円); 2012年度: 2,470千円 (直接経費: 1,900千円、間接経費: 570千円)
• キーワード: プログラム理論 / 圏論 / 関数プログラム / 情報学基礎 / 多相型 / 代数理論 / 構造再帰 / 半構造データ / 原始再帰 / 依存型 / データ構造 / プログラム意味論 / 自動定理証明

研究成果の概要

情報システムが重要な社会基盤の一つとなるにつれ、ソフトウェアの安全性保証が大きな課題となっている。本研究は、信頼性のあるソフトウェアの理論的基礎を確立するために、安全性が保証されたプログラムを構成するための理論を与える事を目的とした。このために従来よりも厳密にデータの定義ができる依存データ型(dependent types)の代数的モデルを明らかにし、その応用を与えた。

研究成果

• [国際共同研究] University of Cambridge(United Kingdom)
• [雑誌論文] Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories (2016)
  • 著者名/発表者名: Makoto Hamana
  • 雑誌名: Formal Structures for Computation and Deduction 巻: LIPIcs ページ: 1-17
  • 査読あり / オープンアクセス
• [雑誌論文] Iteration Algebras for UnQL Graphs and Completeness for Bisimulation (2015)
  • 著者名/発表者名: Makoto Hamana
  • 雑誌名: Electronic Proceedings in Theoretical Computer Science 巻: 191 ページ: 75-89
  • DOI: 10.4204/eptcs.191.8
  • 査読あり / オープンアクセス
• [雑誌論文] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic (2013)
  • 著者名/発表者名: M. Fiore and M. Hamana
  • 雑誌名: Proc. of Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013) 巻: 2013 ページ: 520-529
  • DOI: 10.1109/lics.2013.59
  • 査読あり
• [雑誌論文] Correct Looping Arrows from Cyclic Terms : Traced Categorical Interpretation in Haskell (2012)
  • 著者名/発表者名: M. Hamana
  • 雑誌名: Functional and Logic Programming 巻: LNCS 7294 ページ: 136-150
  • 査読あり
• [学会発表] Iteration Algebras for UnQL Graphs and Completeness for Bisimulation (2016)
  • 著者名/発表者名: 浜名誠
  • 学会等名: メタプログラムに対する論理学的アプローチ研究集会
  • 発表場所: 東北大学電気通信研究所
  • 年月日: 2016-09-27
• [学会発表] プログラミング言語研究のための(高階)項書換え系入門 (2016)
  • 著者名/発表者名: 浜名誠
  • 学会等名: 第18回プログラミングおよびプログラミング言語ワークショップ(PPL'16)
  • 発表場所: 岡山県 玉野市
  • 年月日: 2016-03-07
• [学会発表] Iteration Algebras for UnQL Graphs and Completeness for Bisimulation (2015)
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: The 10th International Workshop on Fixed Points in Computer Science (FICS'15)
  • 発表場所: Technische Universitat Berlin, Germany
  • 年月日: 2015-09-11
  • 国際学会
• [学会発表] A Sound and Complete Equational Axiomatisation of Cyclic Semi-structured Data (2015)
  • 著者名/発表者名: 浜名誠
  • 学会等名: メタプログラムに対する論理学的アプローチ
  • 発表場所: 東北大学 電気通信研究所
  • 年月日: 2015-02-24
• [学会発表] Polymorphic Abstract Syntax via Grothendieck Construction (2013)
  • 著者名/発表者名: M. Hamana
  • 学会等名: プログラミングおよびプログラミング言語ワークショップPPL2013
  • 発表場所: 会津若松御宿東鳳
  • 年月日: 2013-03-06
• [学会発表] Constructing Correct Looping Arrows from Cyclic Terms : Traced Categorical Interpretation in Haskell (2012)
  • 著者名/発表者名: M. Hamana
  • 学会等名: Symposium on Symbolic Computation and Software Science
  • 発表場所: 筑波大学
  • 年月日: 2012-06-03
• [学会発表] Correct Looping Arrows from Cyclic Terms : Traced Categorical Interpretation in Haskell (2012)
  • 著者名/発表者名: M. Hamana
  • 学会等名: Functional and Logic Programming
  • 発表場所: 神戸大学
  • 年月日: 2012-05-23
• [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'13)
  • 発表場所: New Orleans, USA
• [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: Category Theory Conference (CT'13)
  • 発表場所: Macquarie University, Sydney, Australia
• [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: General Algebra and Its Applications (GAIA'13)
  • 発表場所: La Trobe University, Melbourne, Australia
• [学会発表] 多元宇宙多相型代数理論
  • 著者名/発表者名: 浜名誠
  • 学会等名: 日本ソフトウェア科学会第30回大会
  • 発表場所: 東京大学
• [学会発表] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: NII Shoan Workshop on Coinduction for computation structures and programming languages
  • 発表場所: 湘南国際村
• [備考] Makoto Hamana Home Page
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/
• [備考]
  • URL: http://wwww.cs.gunma-u.ac.jp/~hamana/