How to Prove Your Calculus is Decidable: Practical Applications of Second-order Algebraic Theories
Proceedings of the ACM on Programming Languages,
Volume 1, Issue ICFP, September 2017, Article No. 22, pp.1-28, ACM Press, 2017.
Paper in the ACM Digital Library
Slides of my talk.
Recorded live streaming of my talk at ICFP'17 (in Oxford University Podcasts).
A Functional Implementation of Function-as-Constructor
Higher-Order Unification ,
International Workshop on Unification
a part of
FSCD'17, Oxford, 2017.
Slides of a talk at UNIF'17.
Strongly Normalising Cyclic Data Computation
by Iteration Categories of
Second-Order Algebraic Theories,
The 1st International Conference on Formal Structures for Computation and Deduction
the Leibniz International Proceedings in Informatics (LIPIcs), Vol . 52,
Slides of a talk at FSCD'16.
Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic,
(with Marcelo Fiore)
Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science,
pp.520-529, IEEE Computer Society, 2013.
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
Lecture Notes in Computer Science 7294, pp.136-150, Springer, 2012.
Slides of a talk at FLOPS'12.
Polymorphic Abstract Syntax via Grothendieck Construction,
14th International Conference on
Foundations of Software Science and Computation Structures,
Lecture Notes in Computer Science 6604, pp.381-395, Springer-Verlag, 2011.
Slides of a talk at FoSSaCS'11,
Slides of a talk at PPL'13.
Semantic Labelling for Proving Termination of Combinatory Reduction Systems,
18th International Workshop on Functional and
(Constraint) Logic Programming
Lecture Notes in Computer Science 5979, pp.62-78,
Slides of a talk at WFLP'09.
Initial Algebra Semantics for Cyclic Sharing Structures,
Ninth International Conference on Typed Lambda Calculi and Applications
Lecture Notes in Computer Science 5608, pp.127-141,
Slides of a talk at TLCA'09.
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,
Slides of a talk at PPDP'07.
Representing Cyclic Structures as Nested Datatypes,
(with N. Ghani,
T. Uustalu, V. Vene)
Proceedings of 7th Symposium on Trends in Functional Programming
pp. 173-188, University of Nottingham, April 2006.
Universal Algebra for Termination of Higher-Order Rewriting,
16th International Conference on Rewriting Techniques and Applications
Lecture Notes in Computer Science 3467, Springer, pp. 135-149, 2005.
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.
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,
Semantics for Interactive Higher-order Functional-logic Programming,
Doctoral Thesis, University of Tsukuba, 1998.
Algebraic Semantics for Higher-Order Functional-Logic Programming,
Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming, World Scientific, Singapore, pp. 194-209, 1996.
Abstract: English, Japanese
Available: DVI, PS,PDF
M. Hamana, Semantics of a Functional-Logic Programming Language,
Master Thesis, University of Tsukuba, 1995.
(with T. Nishioka, K. Nakahara, A. Middeldorp and T.Ida)
$B>pJs=hM}3X2qO@J8;o(B (Transactions of Information Processing Society of Japan), Vol. 36, No. 8, 1897-1905, in Japanese, pp. 1897-1905, 1995.
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
Department of Computer Science, Faculty of Engineering,
1-5-1 Tenjincho Kiryu, Gunma 376-8515,
E-mail: hamana ## cs.gunma-u.ac.jp (replace ## with @)