ディペンデント型によるディペンダビリティ保証付きデータ構造の理論

2011 年度 研究成果報告書

• 研究課題/領域番号: 22700004
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 群馬大学
• 研究代表者: 浜名 誠 群馬大学, 大学院・工学研究科, 助教 (90334135)
• 研究期間 (年度): 2010 – 2011
• キーワード: データ構造 / 情報基礎 / 自動定理証明 / 関数プログラム

研究概要

信頼性のあるソフトウェアの理論的基礎を確立するために、依存データ型(ディペンデント型)と呼ばれる従来よりも厳密にデータの定義ができるデータ型を用い、信頼性のあるデータ構造とその理論を与えた。

研究成果

• [雑誌論文] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell. Functional and Logic Programming, Lecture Notes in Computer Science (2012)
  • 著者名/発表者名: M. Hamana
  • 雑誌名: Springe-Verlagr 巻: 7294 ページ: 136-150
  • 査読あり
• [雑誌論文] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach, Proc. of 7th ACM SIGPLAN International Workshop on Generic Porgramming (2011)
  • 著者名/発表者名: Makoto Hamana, and Marcelo Fiore.
  • 雑誌名: ACM Press ページ: 59-70
  • 査読あり
• [雑誌論文] Polymorphic Abstract Syntax via Grothendieck Construction. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science (2011)
  • 著者名/発表者名: M. Hamana
  • 雑誌名: Springer-Verlag 巻: 6604 ページ: 381-395
  • 査読あり
• [雑誌論文] Initial Algebra Semantics for Cyclic Sharing Tree Structures. (2010)
  • 著者名/発表者名: M. Hamana
  • 雑誌名: Logical Methods in Computer Science 巻: Volume 6, Issue(3:15) ページ: 1-23
  • 査読あり
• [雑誌論文] Semantic Labelling for Proving Termination of Combinatory Reduction Systems, Functional and Constraint Logic Programming, Lecture Notes in Computer Science (2010)
  • 著者名/発表者名: M. Hamana
  • 雑誌名: Springer-Verlag 巻: 5979 ページ: 62-78
  • 査読あり
• [学会発表] Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell (2012)
  • 学会等名: Symposium on Symbolic Computation and Software Science
  • 発表場所: 筑波大学
  • 年月日: 2012-06-03
• [学会発表] Correct Looping Arrows from Cyclic Terms:Traced Categorica l Interpretation in Haskell (2012)
  • 学会等名: 11th International Symposium on Functional and Logic Programming (FLOPS'12)
  • 発表場所: 神戸大学
  • 年月日: 2012-05-23
• [学会発表] Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell (2012)
  • 学会等名: 14th JSSST Workshop on Programming and Programming Languages(PPL'12)
  • 発表場所: 南紀白浜
  • 年月日: 2012-03-08
• [学会発表] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach (2011)
  • 学会等名: ACM SIGPLAN International Workshop on Generic Porgramming (WGP'11)
  • 発表場所: National Institute of Informatics
  • 年月日: 20110000
• [学会発表] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • 学会等名: 14th International Conference on Foundations of Software Science and Computation Structures
  • 発表場所: Saarbruecken
  • 年月日: 20110000
• [学会発表] Dependent Polynomial Functors for Inductive Families (2011)
  • 学会等名: Shonan Meeting on Dependently Typed Programming and Agda Implementors
  • 発表場所: 湘南国際村
  • 年月日: 2011-09-14
• [学会発表] Dependent Polymorphism (2010)
  • 学会等名: 日本ソフトウェア科学会第27回大会
  • 年月日: 20100900
• [学会発表] Representing Polymorphic Higher-Order Abstract Syntax in Agda and Presheaves (2010)
  • 学会等名: 6th Theorem Proving and Provers eeting (TPP'10)
  • 発表場所: 名古屋大学
  • 年月日: 2010-11-25
• [図書] チューリングを読む-コンピュータサイエンスの金字塔を楽しもう (2012)
  • 著者名/発表者名: チャールズ・ペゾルド (著), 井田哲雄, 鈴木大郎, 奥居哲, 浜名誠, 山田俊行 (訳)
  • 総ページ数: 612
  • 出版者: 日経BP社
• [備考]
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/