J-GLOBAL         Last updated: Nov 16, 2018 at 13:11
Gunma University
Graduate School of Engineering, Department of Computer Science
Job title
Associate Professor
Ph.D(University of Tsukuba)

Research Areas


Academic & Professional Experience

Apr 1998
Mar 2001
JSPS Research Fellow PD, Department of Informatics, Kyoto University, Japan Society for Promotion of Science
Apr 1999
Feb 2001
Visiting Academic, Laboratory for Foundation of Computer Science, LFCS, Univerity of Edinburgh, Scotland


Graduate School, Division of Engineering, University of Tsukuba

Committee Memberships

13th International Symposium on Functional and Logic Programming (FLOPS'16)  program committee member
5th International Workshop on Mathematically Structured Functional Programming (MSFP'14)  program committee member
16th Workshop on Programming and Programming Languages (PPL 2014)  PC member
2nd International Workshop on Haskell and Rewriting Techniques (HART'14)  program committee member
14th Workshop on Programming and Programming Languages (PPL 2012)  PC member

Awards & Honors

Nov 2018
JSSST 2018 Takasahi Award, Japan Society for Software Science and Technology
Sep 2018
JSSST 2018 Best Presentation Award, Japan Society for Software Science and Technology
Winner: Makoto Hamana
May 2018
"Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation", Best paper award, FLOPS 2018
Mar 2016
PPL presentation award
Nov 2012
Foundations of Dependable Software by Dependent Types, Yokoyama Science and Technology Award, Gunma University

Published Papers

T. Aoto, M. Hamana, N. Hirokawa, A. Middeldorp J. Nagele, N. Nishida, K. Shintani, and H. Zankl
the Leibniz International Proceedings in Informatics (LIPIcs)   108 32:1-32:5   Jul 2018   [Refereed]
We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.
Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation
14th International Symposium on Functional and Logic Programming (FLOPS 2018),   Lecture Notes in Computer Scie 99-115   May 2018   [Refereed]
Mathematical Structures in Computer Science   28(2) 287-337   2018   [Refereed]
How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories and Computation
Makoto Hamana
Proceedings of the ACM on Programming Languages   1(22) 1-28   Sep 2017   [Refereed]
We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool SOL, Second-Order Laboratory, which as...
A Functional Implementation of Function-as-Constructor Higher-Order Unification
Makoto Hamana
Proc. International Workshop on Unification (UNIF'17)   1-6   Sep 2017   [Refereed]
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
Makoto Hamana
Logical Methods in Computer Science   13(8) 1-38   2017   [Refereed]
Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theoryies
Hamana Makoto
The 1st International Conference on Formal Structures for Computation and Deduction (FSCD'16)      Apr 2016   [Refereed]
Electronic Proceedings in Theoretical Computer Science   (191) 75-89   Sep 2015   [Refereed]
Marcelo Fiore, Makoto Hamana
Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013)   520-529   Jul 2013   [Refereed]
We formalise and study the notion of polymorphic algebraic theory, as
understood in the mathematical vernacular as a theory presented by equations
between polymorphically-typed terms with both type and term variable binding.

The prototypical exam...
Makoto Hamana
Functional and Logic Programming (FLOPS 2012), Lecture Notes in Computer Science 7294   7294 136-150   2012   [Refereed]
Arrows involving a loop operator provide an interesting programming
methodology for looping computation. On the other hand, Haskell can
define cyclic data structures by recursive definitions. This paper shows
that there exists a common principle ...
M. Hamana
Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science   6604 381-395   2011
Marcelo Fiore, Makoto Hamana
Proc. of 7th ACM SIGPLAN Workshop on Generic Programming (WGP 2011)   59-70   2011   [Refereed]
Every Algebraic Datatype (ADT) is characterised as the initial algebra of
a polynomial functor on sets. This paper extends the characterisation to
the case of more advanced datatypes: Generalised Algebraic
Datatypes (GADTs) and Inductive Families...
M. Hamana
Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science   5979 62-78   2010   [Refereed]
M. Hamana
Typed Lambda Calculi and Applications   Lecture Notes in Computer Science 5608 127-141   2009
Makoto Hamana
Lecture Notes in Computer Science   5608 127-141   2009
Makoto Hamana
Lecture Notes in Computer Science   5979 62-78   2009   [Refereed]
M. Hamana
Proc. of Ninth ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'07)   97-108   2007
K. Matsuda, Z. Hu, K. Nakano, M. Hamana, M. Takeichi
Proc. of 12th ACM SIGPLAN International Conference on Functional Programming (ICFP'07)   47-58   2007
Representing Cyclic Structures as Nested Datatypes
HAMANA MAKOTO / Neil Ghani / Tarmo Uustalu / Varmo Vene
Trends in Functional Programming   pp. 173-188    2006
Higher-Order and Symbolic Computation, Springer Science+Business Media   Volume 19, Issue 2/3    2006


Term Rewriting with Variable Binding
Proceedings of The First International Workshop on Higher-Order Rewriting (HOR'02)      2002

Research Grants & Projects

Modularity for Mata-Programming
Grant-in-Aid for Scientific Research
Project Year: 2004 - 2007
Ministry of Education, Culture, Sports, Science and Technology: Grants-in-Aid for Scientific Research(若手研究(B))
Project Year: 2007 - 2009    Investigator(s): Makoto HAMANA
Cyclic sharing tree structures appear very often in logic and theoretical computer science. We investigate a mathematically clean representation of them. We apply the obtained representation to inductive datatypes in functional programming languages.