Foundations of Dependable Datatypes by Dependent Types

• Project/Area Number: 24300001
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Partial Multi-year Fund
• Section: 一般
• Research Field: Fundamental theory of informatics
• Research Institution: Gunma University
• Principal Investigator: Makoto Hamana 群馬大学, 大学院理工学府, 助教 (90334135)
• Project Period (FY): 2012-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥6,370,000 (Direct Cost: ¥4,900,000、Indirect Cost: ¥1,470,000); Fiscal Year 2014: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000); Fiscal Year 2013: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000); Fiscal Year 2012: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
• Keywords: プログラム理論 / 圏論 / 関数プログラム / 情報学基礎 / 多相型 / 代数理論 / 構造再帰 / 半構造データ / 原始再帰 / 依存型 / データ構造 / プログラム意味論 / 自動定理証明

Outline of Final Research Achievements

In order to establish fundamentals of dependable software systems, we aim to establish theories of dependable software. We develop foundations and applications of dependent types by clarifying algebraic models of types and equational theories of dependent types.

Research Products

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