Semantics of Core Haskell -- Towards Foundations of Verification of Advanced Functional Programs

• Project/Area Number: 25540002
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Theory of informatics
• Research Institution: Gunma University
• Principal Investigator: Makoto Hamana 群馬大学, その他部局等, 助教 (90334135)
• Co-Investigator(Kenkyū-buntansha): SHINYA KATSUMATA 京都大学, 数理解析研究所, 助教 (30378963)
• Project Period (FY): 2013-04-01 – 2016-03-31
• Project Status: Completed (Fiscal Year 2015)
• Budget Amount: ¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000); Fiscal Year 2015: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000); Fiscal Year 2014: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2013: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
• Keywords: プログラム理論 / 圏論 / 関数プログラム / 情報学基礎 / Haskell / プログラム意味論 / 操作的意味論

Outline of Final Research Achievements

In order to establish dependable software systems, we need to establish mathematical models and their theories. We develop various theories of functional programming through exploring mathematical models of Haskell's core language.

Research Products

• [Journal Article] Towards a Formal Theory of Graded Monads (2016)
  • Author(s): Soichiro Fujii, Shin-ya Katsumata, and Paul-Andre Mellies
  • Journal Title: Lecture Notes in Computer Science Volume: 9634 Pages: 513-530
  • DOI: 10.1007/978-3-662-49630-5_30
  • ISBN: 9783662496299, 9783662496305
  • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
• [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] Codensity Liftings of Monads (2015)
  • Author(s): Shin-ya Katsumata, Tetsuya Sato
  • Journal Title: Algebra and Coalgebra in Computer Science (CALCO 2015) Volume: LIPIcs 35 Pages: 156-170
  • DOI: 10.4230/LIPIcs.CALCO.2015.156
  • Peer Reviewed
• [Journal Article] Parametric Effect Monads and Semantics of Effect Systems (2014)
  • Author(s): Shin-ya Katsumata
  • Journal Title: Proc. of ACM Symposium on Principles of Programming Languages Volume: POPL 2014 Pages: 633-645
  • Peer Reviewed
• [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
• [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): 浜名誠
  • Organizer: メタプログラムに対する論理学的アプローチ研究集会
  • Place of Presentation: 東北大学 電気通信研究所
  • Year and Date: 2015-09-28
  • Invited
• [Presentation] Iteration Algebras for UnQL Graphs and Completeness for Bisimulation (2015)
  • Author(s): Makoto Hamana
  • Organizer: FireEye Seminar
  • Place of Presentation: FireEye Dresden
  • Year and Date: 2015-09-15
• [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] Algebraic Semantics of Higher-order Abstract Syntax and Second-order Rewriting (2015)
  • Author(s): Makoto Hamana
  • Organizer: International Summer School on Rewriting (ISR 2015)
  • Place of Presentation: Leipzig, Germany
  • Year and Date: 2015-08-10
  • Int'l Joint Research
• [Presentation] Codensity Liftings of Monads (2015)
  • Author(s): Shin-ya Katsumata
  • Organizer: 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
  • Place of Presentation: Nijmegen, The Netherlands
  • Year and Date: 2015-06-24
  • Int'l Joint Research
• [Presentation] モナド、代数理論と計算効果 (2015)
  • Author(s): 勝股 審也
  • Organizer: 第17回プログラミングおよびプログラミング言語ワークショップ PPL 2015
  • Place of Presentation: 道後プリンスホテル
  • Year and Date: 2015-03-04
• [Presentation] Sound and Complete Equational Axiomatisation of Cyclic Semi-structured Data (2015)
  • Author(s): 浜名誠
  • Organizer: メタプログラムに対する論理学的アプローチ
  • Place of Presentation: 東北大学 電気通信研究所
  • Year and Date: 2015-02-24
• [Presentation] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
  • Author(s): Makoto Hamana
  • Organizer: ACM/IEEE Symposium on Logic in Computer Science
  • Place of Presentation: Tulane University, New Orleans, USA
• [Presentation] Parametric Effect Monads and Semantics of Effect Systems
  • Author(s): Shin-ya Katsumata
  • Organizer: ACM Symposium on Principles of Programming Languages
  • Place of Presentation: San Diego, USA
• [Presentation] Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic
  • Author(s): Makoto Hamana
  • Organizer: NII Shonan Meeting on Coinduction for Computation Structures and Programming Languages
  • Place of Presentation: 湘南国際村
• [Presentation] Categorical TT-lifting and Preorders on Monads
  • Author(s): Shin-ya Katsumata
  • Organizer: NII Shonan Meeting on Coinduction for Computation Structures and Programming Languages
  • Place of Presentation: 湘南国際村
• [Presentation] Logical Relations for Monads by Categorical TT-Lifting
  • Author(s): Shin-ya Katsumata
  • Organizer: The fifth workshop on Mathematically Structured Functional Programming
  • Place of Presentation: Grenoble, France
  • Invited
• [Presentation] On Multiversal Polymorphic Algebraic Theories
  • Author(s): Makoto Hamana
  • Organizer: メタプログラムに対する論理的アプローチ研究会
  • Place of Presentation: 東北大学電気通信研究所
  • Invited
• [Presentation] Polymorphic Algebraic Theories and Logical Predicates
  • Author(s): Makoto Hamana
  • Organizer: Semantic Methods in Haskell and Functional Programming Seminar
  • Place of Presentation: 国立情報学研究所
• [Presentation] Parametric Effect Monads and Semantics of Effect Systems
  • Author(s): Shin-ya Katsumata
  • Organizer: Semantic Methods in Haskell and Functional Programming Seminar
  • Place of Presentation: 国立情報学研究所
• [Remarks] Makoto Hamana Home Page
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/
• [Remarks] 研究会
  • URL: http://www.cs.gunma-u.ac.jp/~hamana/Semhas/