Dependable Data Structures by Dependent Types

• Project/Area Number: 22700004
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Fundamental theory of informatics
• Research Institution: Gunma University
• Principal Investigator: HAMANA Makoto 群馬大学, 大学院・工学研究科, 助教 (90334135)
• Project Period (FY): 2010 – 2011
• Project Status: Completed (Fiscal Year 2011)
• Budget Amount: ¥3,900,000 (Direct Cost: ¥3,000,000、Indirect Cost: ¥900,000); Fiscal Year 2011: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000); Fiscal Year 2010: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
• Keywords: データ構造 / 情報基礎 / 自動定理証明 / 関数プログラム / 依存型 / 情報学基礎

Research Abstract

Dependent types are data types which ensure more precise properties of data thanordinary data types. Using dependent types, we develop a theory and applications ofdependable data structures, aiming to establish foundations of reliable computer softwares.

Research Products

• [Journal Article] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell. Functional and Logic Programming, Lecture Notes in Computer Science (2012)
  • Author(s): M. Hamana
  • Journal Title: Springe-Verlagr Volume: 7294 Pages: 136-150
  • Peer Reviewed
• [Journal Article] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell (2012)
  • Author(s): Makoto Hamana,
  • Journal Title: Functional and Logic Programming Volume: LNCS 7294 Pages: 136-150
  • Peer Reviewed
• [Journal Article] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach, Proc. of 7th ACM SIGPLAN International Workshop on Generic Porgramming (2011)
  • Author(s): Makoto Hamana, and Marcelo Fiore.
  • Journal Title: ACM Press Pages: 59-70
  • Peer Reviewed
• [Journal Article] Polymorphic Abstract Syntax via Grothendieck Construction. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science (2011)
  • Author(s): M. Hamana
  • Journal Title: Springer-Verlag Volume: 6604 Pages: 381-395
  • Peer Reviewed
• [Journal Article] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach (2011)
  • Author(s): Makoto Hamana, Marcelo Fiore
  • Journal Title: Generic Programming Volume: WGP'11 Pages: 59-70
  • DOI: 10.1145/2036918.2036927
  • Peer Reviewed
• [Journal Article] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • Author(s): M.Hamana
  • Journal Title: Foundations of Software Science and Computation Structures Volume: LNCS 6604 Pages: 381-395
  • Peer Reviewed
• [Journal Article] Initial Algebra Semantics for Cyclic Sharing Tree Structures. (2010)
  • Author(s): M. Hamana
  • Journal Title: Logical Methods in Computer Science Volume: Volume 6, Issue(3:15) Pages: 1-23
  • Peer Reviewed
• [Journal Article] Semantic Labelling for Proving Termination of Combinatory Reduction Systems, Functional and Constraint Logic Programming, Lecture Notes in Computer Science (2010)
  • Author(s): M. Hamana
  • Journal Title: Springer-Verlag Volume: 5979 Pages: 62-78
  • Peer Reviewed
• [Journal Article] Initial Algebra Semantics for Cyclic Sharing Tree Structures (2010)
  • Author(s): M.Hamana
  • Journal Title: Logical Methods in Computer Science Volume: Vol.6(3:15) Pages: 1-23
  • Peer Reviewed
• [Presentation] Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell (2012)
  • Organizer: Symposium on Symbolic Computation and Software Science
  • Place of Presentation: 筑波大学
  • Year and Date: 2012-06-03
• [Presentation] Correct Looping Arrows from Cyclic Terms:Traced Categorica l Interpretation in Haskell (2012)
  • Organizer: 11th International Symposium on Functional and Logic Programming (FLOPS'12)
  • Place of Presentation: 神戸大学
  • Year and Date: 2012-05-23
• [Presentation] Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell (2012)
  • Organizer: 14th JSSST Workshop on Programming and Programming Languages(PPL'12)
  • Place of Presentation: 南紀白浜
  • Year and Date: 2012-03-08
• [Presentation] Dependent Polynomial Functors for Inductive Families (2011)
  • Organizer: Shonan Meeting on Dependently Typed Programming and Agda Implementors
  • Place of Presentation: 湘南国際村
  • Year and Date: 2011-09-14
• [Presentation] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • Author(s): M.Hamana
  • Organizer: Foundations of Software Science and Computation Structures
  • Place of Presentation: ドイツ ザールブリュッケンサーランド大学
  • Year and Date: 2011-03-30
• [Presentation] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach (2011)
  • Organizer: ACM SIGPLAN International Workshop on Generic Porgramming (WGP'11)
  • Place of Presentation: National Institute of Informatics
• [Presentation] Polymorphic Abstract Syntax via Grothendieck Construction (2011)
  • Organizer: 14th International Conference on Foundations of Software Science and Computation Structures
  • Place of Presentation: Saarbruecken
• [Presentation] Representing Polymorphic Higher-Order Abstract Syntax in Agda and Presheaves (2010)
  • Organizer: 6th Theorem Proving and Provers eeting (TPP'10)
  • Place of Presentation: 名古屋大学
  • Year and Date: 2010-11-25
• [Presentation] Dependent Polymorphism (2010)
  • Author(s): M.Hamana
  • Organizer: 日本ソフトウェア科学会第27回大会
  • Place of Presentation: 津田塾大学
  • Year and Date: 2010-09-15
• [Presentation] Another Initial Algebra Semantics of Inductive Families for Programming (2010)
  • Author(s): M.Hamana
  • Organizer: Dependently Typed Programming 2010
  • Place of Presentation: イギリス エジンバラ大学
  • Year and Date: 2010-07-10
• [Presentation] Dependent Polymorphism (2010)
  • Organizer: 日本ソフトウェア科学会第27回大会
• [Presentation] Dependent Polynomial Functors for Inductive Families
  • Author(s): Makoto Hamana
  • Organizer: Dependently Typed Programming/Agda Implementors Meeting, Shonan Meeting Seminar
  • Place of Presentation: 湘南国際村
  • Invited
• [Presentation] A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach
  • Author(s): Makoto Hamana
  • Organizer: the seventh ACM SIGPLAN workshop on Generic programming
  • Place of Presentation: National Institute of Informatics
• [Presentation] Constructing Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell
  • Author(s): Makoto Hamana
  • Organizer: Symposium on Symbolic Computation and Software Science
  • Place of Presentation: 筑波大学
  • Invited
• [Presentation] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell
  • Author(s): Makoto Hamana
  • Organizer: プログラミングおよびプログラミング言語ワークショップ PPL2012
  • Place of Presentation: 南紀白浜むさし
• [Presentation] Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell
  • Author(s): Makoto Hamana
  • Organizer: Functional and Logic Programming
  • Place of Presentation: 神戸大学
• [Book] チューリングを読む-コンピュータサイエンスの金字塔を楽しもう (2012)
  • Author(s): チャールズ・ペゾルド (著), 井田哲雄, 鈴木大郎, 奥居哲, 浜名誠, 山田俊行 (訳)
  • Total Pages: 612
  • Publisher: 日経BP社
• [Book] チューリングを読む (2012)
  • Author(s): チャールズ・ペゾルド (著), 井田哲雄, 鈴木大郎, 奥居哲, 浜名誠, 山田俊行(訳)
  • Total Pages: 612
  • Publisher: 日経BP
• [Remarks]
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/
• [Remarks]
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/