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

• 研究課題/領域番号: 22700004
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 群馬大学
• 研究代表者: 浜名 誠 群馬大学, 大学院・工学研究科, 助教 (90334135)
• 研究期間 (年度): 2010 – 2011
• 研究課題ステータス: 完了 (2011年度)
• 配分額: 3,900千円 (直接経費: 3,000千円、間接経費: 900千円); 2011年度: 1,820千円 (直接経費: 1,400千円、間接経費: 420千円); 2010年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
• キーワード: データ構造 / 情報基礎 / 自動定理証明 / 関数プログラム / 依存型 / 情報学基礎

研究概要

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

研究成果

• [雑誌論文] 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
  • 査読あり
• [雑誌論文] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell (2012)
  • 著者名/発表者名: Makoto Hamana,
  • 雑誌名: Functional and Logic Programming 巻: LNCS 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
  • 査読あり
• [雑誌論文] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach (2011)
  • 著者名/発表者名: Makoto Hamana, Marcelo Fiore
  • 雑誌名: Generic Programming 巻: WGP'11 ページ: 59-70
  • DOI: 10.1145/2036918.2036927
  • 査読あり
• [雑誌論文] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • 著者名/発表者名: M.Hamana
  • 雑誌名: Foundations of Software Science and Computation Structures 巻: LNCS 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
  • 査読あり
• [雑誌論文] Initial Algebra Semantics for Cyclic Sharing Tree Structures (2010)
  • 著者名/発表者名: M.Hamana
  • 雑誌名: Logical Methods in Computer Science 巻: Vol.6(3:15) ページ: 1-23
  • 査読あり
• [学会発表] 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
• [学会発表] Dependent Polynomial Functors for Inductive Families (2011)
  • 学会等名: Shonan Meeting on Dependently Typed Programming and Agda Implementors
  • 発表場所: 湘南国際村
  • 年月日: 2011-09-14
• [学会発表] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • 著者名/発表者名: M.Hamana
  • 学会等名: Foundations of Software Science and Computation Structures
  • 発表場所: ドイツ ザールブリュッケンサーランド大学
  • 年月日: 2011-03-30
• [学会発表] 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
• [学会発表] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • 学会等名: 14th International Conference on Foundations of Software Science and Computation Structures
  • 発表場所: Saarbruecken
• [学会発表] Representing Polymorphic Higher-Order Abstract Syntax in Agda and Presheaves (2010)
  • 学会等名: 6th Theorem Proving and Provers eeting (TPP'10)
  • 発表場所: 名古屋大学
  • 年月日: 2010-11-25
• [学会発表] Dependent Polymorphism (2010)
  • 著者名/発表者名: M.Hamana
  • 学会等名: 日本ソフトウェア科学会第27回大会
  • 発表場所: 津田塾大学
  • 年月日: 2010-09-15
• [学会発表] Another Initial Algebra Semantics of Inductive Families for Programming (2010)
  • 著者名/発表者名: M.Hamana
  • 学会等名: Dependently Typed Programming 2010
  • 発表場所: イギリス エジンバラ大学
  • 年月日: 2010-07-10
• [学会発表] Dependent Polymorphism (2010)
  • 学会等名: 日本ソフトウェア科学会第27回大会
• [学会発表] Dependent Polynomial Functors for Inductive Families
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: Dependently Typed Programming/Agda Implementors Meeting, Shonan Meeting Seminar
  • 発表場所: 湘南国際村
  • 招待講演
• [学会発表] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: the seventh ACM SIGPLAN workshop on Generic programming
  • 発表場所: National Institute of Informatics
• [学会発表] Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: Symposium on Symbolic Computation and Software Science
  • 発表場所: 筑波大学
  • 招待講演
• [学会発表] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: プログラミングおよびプログラミング言語ワークショップ PPL2012
  • 発表場所: 南紀白浜むさし
• [学会発表] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell
  • 著者名/発表者名: Makoto Hamana
  • 学会等名: Functional and Logic Programming
  • 発表場所: 神戸大学
• [図書] チューリングを読む-コンピュータサイエンスの金字塔を楽しもう (2012)
  • 著者名/発表者名: チャールズ・ペゾルド (著), 井田哲雄, 鈴木大郎, 奥居哲, 浜名誠, 山田俊行 (訳)
  • 総ページ数: 612
  • 出版者: 日経BP社
• [図書] チューリングを読む (2012)
  • 著者名/発表者名: チャールズ・ペゾルド (著), 井田哲雄, 鈴木大郎, 奥居哲, 浜名誠, 山田俊行(訳)
  • 総ページ数: 612
  • 出版者: 日経BP
• [備考]
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/
• [備考]
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/