Makoto Hamana

Professor at Department of Computer Science and Networks, Kyushu Institute of Technology
[履歴書(jp) / CV(english)] (@Research map) [JGLOBAL] [DBLP] [Google Scholar]

Research Interests

• General: mathematical foundations of programming languages
• Theory and practice of functional programming, especially Haskell and Agda
• Higher-order abstract syntax and Fiore-Plotkin-Turi style semantics
• Higher-order rewriting and its categorical algebraic semantics

News

• I moved to Kyushu Institute of Technology, started a new laboratory for programming languages and applied semantics. (2024.4.1)
• 日本学術振興会 科研費 基盤(B) 研究課題「高階書換え系による次世代マルチパラダイム・プログラミング言語の展開」採択されました。(2024.3.1)
  
• Our new paper on Term Evaluation and Refinements Systems (with Koko Muroya) will be presented at FLOPS'24 Kumamoto.
• Second-order computation analyser SOL (web interface) based on the WebCUI framework.
• 日本ソフトウェア科学会第40回大会 優秀発表賞 を受賞しました。(2023.11)
• I gave a talk "Verifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory" at Haskell Symposium 2023, Seatell, USA.
• I gave a talk on the complete algebraic semantics of second-order rewriting at SYCO10 at Edinburgh University, Slides.
• I serve as a PC member of The ACM SIGPLAN Haskell Symposium 2022 .
• I serve as a PC member of 11th International Workshop on Confluence (IWC'22) .
• PPL 2021で研究室の4年生の藤岡 亮君が 「高階パターン単一化のUnboundライブラリを用いたHaskellによる実装」 のポスター発表します。 実装 at GitHub.
• Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and SOL. Extended abstract, Slides, Video. An invited talk at 15th International Symposium on Functional and Logic Programming (FLOPS'20), presented on 8, September, 2020.
• Postdoc/internship positions available. If you are interested in working on SOL or related matter with us, please contact me.
• I serve as a PC member of the 25th ACM SIGPLAN International Conference on Functional Programming (ICFP'20) .
• I serve as a PC member of 11th International Workshop on Computing with Terms and Graphs (TERMGRAPH'20) .
• I serve as a PC member of 9th International Workshop on Confluence (IWC'20) .
• Our tool SOL participated Confluence Competition (CoCo'18) and Termination Competition 2018, which is developed by SOL Team 2018: Makoto Hamana, and Kentaro Kikuchi. SOL's results: confluence (HRS category) , termination (Higher-order union beta)
• Our paper on foundations of a calculus of graph database was accepted to a journal Mathematical Structures in Computer Science.
• Here are the slides and recorded video of my ICFP'17 talk.
• Our tool SOL participates Confluence Competition (CoCo'17) (Result) and Termination Competition 2017 (Result), developed by SOL Team: Makoto Hamana, Tatsuya Abe, Yuito Murase, and Kazuhiko Sakaguchi.
• チュートリアル プログラミング言語研究のための(高階)項書換え系入門 　[スライド (slides)]
  (Tutorial: Introduction to term rewriting for theories of programming languages)
  (第18回プログラミングおよびプログラミング言語ワークショップ
• I gave a lecture on semantics of higher-order rewriting at International Summer School on Rewriting (ISR 2015) in August 10-14, at Leipzig, Germany. Leipzig was a nice city and I enjoyed lecturing. Here is material of my lecture:
  [A] Slides for lecture 1
  [B] Slides for lecture 2
  [C] Reference.
• Proceedings of Workshop on Higher-Order Rewriting (HOR'12) is available.

Papers      [List in DBLP]

• Foundations of Haskell's Rewrite Rules based on Higher-Kinded Polymorphic Rewrite Systems,
  10th International Symposium on Symbolic Computation in Software Science (SCSS 2024), accepted.
• Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement,
  (with Koko Muroya), 17th International Symposium on Functional and Logic Programming (FLOPS 2024), accepted.
• Complete Algebraic Semantics for Second-Order Rewriting Systems based on Abstract Syntax with Variable Binding,
  Mathematical Structures in Computer Science, Cambridge University Press, 2022.
  Available: PDF, Paper in MSCS site,
• Modular Termination for Second-Order Computation Rules and Application to Algebraic Effect Handlers,
  Logical Methods in Computer Science, Vol. 18, Issue 2, No.8, June 14, 2022.
  Available: Paper in LMCS
• Polymorphic computation systems: Theory and practice of confluence with call-by-value
  (with Tatsuya Abe and Kentaro Kikuchi), Science of Computer Programming, Elsevier, Volume 187, 15 February 2020, 102322.
  Available: PDF, Paper in ScienceDirect.
• How to prove decidability of equational theories with second-order computation analyser SOL
  Journal of Functional Programming, Cambridge University Press, Vol. 29, e20, 2019.
  Available: PDF, Paper in CambridgeCore.
• Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation,
  14th International Symposium on Functional and Logic Programming (FLOPS 2018),
  Lecture Notes in Computer Science 10818, pp.99-115, Springer, 2018. Best Paper Award.
  Available: PDF(Author's version), Slides of my talk.
• The Algebra of Recursive Graph Transformation Language UnCAL: Complete Axiomatisation and Iteration Categorical Semantics,
  (with Kazutaka Matsuda and Kazuyuki Asada), Mathematical Structures in Computer Science, Volume 28, Issue 2, pp.287-337, Cambridge University Press, doi:10.1017/S096012951600027X, 2018.
  Available: Paper in MSCS site.
• Confluence Competition 2018,
  (with T. Aoto, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and H. Zankl), 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), the Leibniz International Proceedings in Informatics (LIPIcs), Vol . 108, pp. 32:1-32:5, 2018.
  Available: Paper in DROPS
• How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation,
  Proceedings of the ACM on Programming Languages, Volume 1, Issue ICFP, September 2017, Article No. 22, pp.1-28, ACM Press, 2017.
  Available: Paper in the ACM Digital Library, Slides of my talk. Recorded live streaming of my talk at ICFP'17 (in Oxford University Podcasts).
  Implementation: PolySOL (web interface)
• A Functional Implementation of Function-as-Constructor Higher-Order Unification ,
  International Workshop on Unification (UNIF'17), a part of FSCD'17, Oxford, 2017.
  Available: PDF, Slides of a talk at UNIF'17.
• Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories,
  Logical Methods in Computer Science, Vol. 13, Issue 4, No.8, pp.1-38, 2017.
  Available: Paper in LMCS
  
• Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories,
  The 1st International Conference on Formal Structures for Computation and Deduction (FSCD'16),
  the Leibniz International Proceedings in Informatics (LIPIcs), Vol . 52, pp.21:1-21:18, 2016.
  Available: PDF, Slides of a talk at FSCD'16.
• Iteration Algebras for UnQL Graphs and Completeness for Bisimulation,
  The 10th International Workshop on Fixed Points in Computer Science (FICS'15), Electronic Proceedings in Theoretical Computer Science 191, pp.75-89, 2015.
  Available: PDF.
• Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic,
  (with Marcelo Fiore)
  Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2013) pp.520-529, IEEE Computer Society, 2013.
  Available: PDF, Slides of a talk at LICS'13.
• Correct Looping Arrows from Cyclic Terms: Traced Categorical Interpretation in Haskell,
  11th International Symposium on Functional and Logic Programming (FLOPS 2012),
  Lecture Notes in Computer Science 7294, pp.136-150, Springer, 2012.
  Available: PDF, Slides of a talk at FLOPS'12. Related codes:
  • Case1: cyclic data structure
  • Case2: circuit
  • Case3: recursive function
  • Case3': recursive function with effect
• A Foundation for GADTs and Inductive Families: Dependent Polynomial Functor Approach,
  (with Marcelo Fiore)
  7th ACM SIGPLAN Workshop on Generic Programming (WGP 2011), pp.59-70, ACM Press, 2011.
  Available: PDF, Slides (at Shonan workshop AIM-DTP'11), Slides (at WGP'11)
• Polymorphic Abstract Syntax via Grothendieck Construction,
  14th International Conference on Foundations of Software Science and Computation Structures, (FoSSaCS 2011),
  Lecture Notes in Computer Science 6604, pp.381-395, Springer-Verlag, 2011.
  Available: PDF, Slides of a talk at FoSSaCS'11, Slides of a talk at PPL'13.
• Initial Algebra Semantics for Cyclic Sharing Tree Structures,
  Logical Methods in Computer Science, Volume 6, Issue 3, No.15, 2010.
  Available: Paper in LMCS
  Related codes:
  1. Graph algorithms based on depth-first search on cyclic sharing trees in Haskell
  2. A dependent type defintion of cyclic sharing trees in Agda
• Semantic Labelling for Proving Termination of Combinatory Reduction Systems,
  18th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2009),
  Lecture Notes in Computer Science 5979, pp.62-78, Springer-Verlag, 2010.
  Available: PDF, Slides of a talk at WFLP'09.
• Initial Algebra Semantics for Cyclic Sharing Structures,
  Ninth International Conference on Typed Lambda Calculi and Applications (TLCA 2009),
  Lecture Notes in Computer Science 5608, pp.127-141, Springer-Verlag, 2009.
  Available: Slides of a talk at TLCA'09.
  
• 補関数の生成による複製機能付きプログラムの自動双方向化 ,
  (with 松田 一孝, 胡 振江, 中野 圭介, 武市 正人)
  コンピュータソフトウェア, Vol. 26, No. 2, pp. 56-75, 2009.
  Available: Paper in J-STAGE
• Bidirectionalization Transformation based on Automatic Derivation of View Complement Functions,
  (with Kazutaka Matsuda, Zhenjiang Hu, Keisuke Nakano, Masato Takeichi)
  12th ACM SIGPLAN International Conference on Functional Programming (ICFP 2007),
  ACM Press, pp.47-58, 2007.
  Available: Paper in the ACM Digital Library, PDF.
• Higher-Order Semantic Labelling for Inductive Datatype Systems,
  Ninth ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming
  (PPDP 2007), ACM Press, pp.97-108, 2007.
  Available: Paper in the ACM Digital Library, PDF, Slides of a talk at PPDP'07.
  
• An Initial Algebra Approach to Term Rewriting Systems with Variable Binders,
  Higher-Order and Symbolic Computation, Springer Science+Business Media,
  Volume 19, Issue 2/3, pp. 231-262, 2006.
  Available: Paper at Springer Link
• Explicit Substitutions and Higher-Order Syntax,
  (with Neil Ghani, Tarmo Uustalu)
  Higher-Order and Symbolic Computation, Springer Science+Business Media,
  Volume 19, Issue 2/3, pp. 263-282, 2006.
  Available: Paper at Springer Link
• Representing Cyclic Structures as Nested Datatypes,
  (with N. Ghani, T. Uustalu, V. Vene)
  Proceedings of 7th Symposium on Trends in Functional Programming (TFP 2006),
  pp. 173-188, University of Nottingham, April 2006.
  Available: PDF
• 高階書換え系の停止性のための代数モデル (第12回日本ソフトウェア科学会論文賞),
  コンピュータソフトウェア, Vol. 23, No. 2, pp. 142-156, 岩波書店, 2006.
  Available: Paper in J-STAGE
  
• Σモノイド─メタ変数と明示的環境を持つ高階構文,
  コンピュータソフトウェア, Vol. 22, No. 3, pp. 201-207, 岩波書店, 2005.
  Available: Paper in J-STAGE
• Universal Algebra for Termination of Higher-Order Rewriting,
  16th International Conference on Rewriting Techniques and Applications (RTA'05),
  Lecture Notes in Computer Science 3467, Springer, pp. 135-149, 2005.
  Available: PDF, Slides of a talk at RTA'05
  
• Free Σ-monoids: A Higher-Order Syntax with Metavariables,
  The Second Asian Symposium on Programming Languages and Systems (APLAS 2004),
  Lecture Notes in Computer Science 3202, Springer, pp. 348-363, 2004.
  Available: PDF
  
• Term Rewriting with Variable Binding: An Initial Algebra Approach,
  Fifth ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming
  (PPDP 2003), ACM Press, pp.148-159, 2003.
  Available: Paper in the ACM Digital Library, DVI, PS
  
• A Logic Programming Language based on Binding Algebras,
  International Symposium on Theoretical Aspects of Computer Software (TACS 2001),
  Lecture Notes in Computer Science 2215, Springer, pp. 243-262, 2001.
  Abstract: English
  
• Semantics for Interactive Higher-order Functional-logic Programming,
  Doctoral Thesis, University of Tsukuba, 1998.
  Abstract: English
  Available: PDF, PS
  
• Equivalence of the Quotient Term Model and the Least Complete Herbrand Model for a Functional-Logic Language,
  Journal of Functional and Logic Programming, Vol. 1997, No. 1, 1997.
  Abstract: Japanese
  Available: Journal page
  
• Algebraic Semantics for Higher-Order Functional-Logic Programming,
  Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming (FLOPS'96), World Scientific, Singapore, pp. 194-209, 1996.
  Abstract: English, Japanese
  Available: DVI, PS, PDF
  
• 項書換え系としての論理プログラム.
  (with 鈴木大郎)
  コンピュータソフトウェア, Vol. 14, No. 6, pp. 29-43, 岩波書店, 1997.
  Available: Paper in J-STAGE
• M. Hamana, Semantics of a Functional-Logic Programming Language,
  Master Thesis, University of Tsukuba, 1995.
  
• 作用型項書換え系に基づく関数論理型言語の設計と実装 (A Design and Implementation of a Functional-Logic Language Based on Applicative Term Rewriting Systems),
  (with T. Nishioka, K. Nakahara, A. Middeldorp and T.Ida)
  情報処理学会論文誌 (Transactions of Information Processing Society of Japan), Vol. 36, No. 8, 1897-1905, in Japanese, pp. 1897-1905, 1995.
  Abstract: Japanese
  Available: PDF
  

Some Talks

• Representing Polymorphic Higher-Order Abstract Syntax in Agda and Presheaves
  6th Theorem Proving and Provers Meeting (TPP'10),
  25 November, 2010, Nagoya University.
• Dependent Polymorphism
  27th Conf. Japan Society for Software Science and Technology (JSSST'10),
  15 September, 2010, Tokyo. Slides.
• Another Initial Algebra Semantics of Inductive Families for Programming
  Dependently Typed Programming 2010, associated with LICS,
  10 July, 2010, Edinburgh.
• Inductive Cyclic Sharing Data Structures
  30 June, 2008. Slides.
• What is the Category for Haskell?
  CAPS, IPL, University of Tokyo, 23 October, 2007. Slides.
• Representing Cyclic Structures as Nested Datatypes,
  
  • 23th Conf. Japan Society for Software Science and Technology (JSSST'06),
    15 September, 2006,
    Takahashi Award for the best presentation and paper (第23回高橋奨励賞)
    
  • 30th Tokyo Programming Seminar, 23 May, 2006.
    Available: Slides, Haskell code

Book

• 井田哲雄, 浜名誠 (共著), 計算モデル論入門 ―チューリング機械からラムダ計算へ―,
  Information Science & Engineering F5 , A5判, 136頁, 1400円, ISBN4-7819-1135-8, サイエンス社.
  [どこから買える？]
  • サポートページ
  • 参考資料 「型付きラムダ計算の停止性」 (2007.12.13改訂)

Miscellaneous

• M. Hamana. Simple beta0-Unification for Terms with Context Holes, UNIF 2002, July 2002, Paper, Slides.
• M. Hamana. Interactive Functional-logic Programming by Conditional Term Rewriting Systems,
  Proceedings of JSSST Workshop on Programming and Programming Languages (PPL'99), 1999.
  Available: DVI, PS
• M. Hamana, Term rewriting with sequences,
  Proceedings of the First International Theorema Workshop, Report Series No. 97-20. RISC-Linz, Johannes Kepler University, 1997.
  Available: DVI, PS

Address

Kyushu Institute of Technology, 680-4 Kawazu, Iizuka, Fukuoka 820-8502, JAPAN
E-mail: hamana ## csn.kyutech.ac.jp (replace ## with @)
WWW: solweb.mydns.jp/hamana/

Links to the places I have worked/stayed

• SCORE at Tsukuba University
  
• Sato's lab. at Kyoto University
• LFCS, University of Edinburgh
• IPL at University of Tokyo
• Gunma University