* Abstract Syntax with Variable Binding
- M. Fiore and G. Plotkin and D. Turi.
Abstract syntax and variable binding, 1999, LICS'99, pp. 193--202.
# The first paper that establishes the algebraic semantics of HOAS.

- M. Hamana.
Free \Sigma-monoids: A higher-order syntax with metavariables.
Programming Languages and Systems}, Lecture Notes in Computer Science  3202, pp. 348-363, Springer-Verlag, 2004.
# Gave a free construction and showed that free Sigma-monoids are HOAS with metavariables.

- M. Hamana.
Universal Algebra for Termination of Higher-Order Rewriting,
Rewriting Techniques and Applications}, Lecture Notes in Computer Science  3467, pp. 135-149, Springer-Verlag, 2005.
# The first sound and complete semantics of CRS

* Typed HOAS, Equational logic, Rewriting
- M. Fiore.
Semantic analysis of normalisation by evaluation for typed lambda calculus,
Proc. of PPDP'02, pp. 26--37, 2002. 
# The first extension of Fiore-Plotkin-Turi semantics to typed HOAS

- M. Miculan and I. Scagnetto.
A Framework for Typed HOAS and Semantics,
PPDP'03, ACM Press, pp. 184--194, 2003.
# More precise description of semantics of typed HOAS

- M. Hamana.
Term Rewriting with Variable Binding: An Initial Algebra Approach,
Proc. of PPDP'03, pp. 148-159, 2003
(Journal ver: Higher-Order and Symb. Comput., Vol. 19, 2006.)
# A simple extension of TRS with binders, affected to Nomial rewriting.

- M. Fiore and C.-K. Hur.
Second-Order Equational Logic, CSL'10, LNCS 6247, pp. 320--335, 2010
# Second-Order equational logic and its complete algebraic semantics

- M. Fiore and O. Mahmoud.
Second-order algebraic theories, MFCS'10, LNCS 6281, pp. 368--380. 2010.
# Another form of second-Order equational logic

- M. Hamana. Polymorphic Abstract Syntax via Grothendieck Construction.
Foundations of Software Science and Computation Structures,
Lecture Notes in Computer Science 6604, pp.381-395, Springer-Verlag, 2011. 
# The first algebraic semaitcs of Polymorphic HOAS.

- M. Fiore and M. Hamana
Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations,
and Equational Logic,
Proc. of Twenty-Eighth Annual ACM/IEEE Symposium on Logic in
Computer Science, (LICS 2013), pp. 520-529, IEEE Computer Society, 2013.
# Polymorphic equational logic and its complete algebraic semantics.

* Applications 
- M. Hamana. 
Higher-Order Semantic Labelling for Inductive Datatype Systems.
Ninth ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 97-108, ACM Press, 2007. 
# Extension of semantic labelling to IDRS

- M. Hamana.
Semantic Labelling for Proving Termination of Combinatory Reduction Systems,
Functional and Constraint Logic Programming}, Lecture Notes in Computer Science
5979, pp.62-78, Springer-Verlag, 2010.
# Extension of semantic labelling to CRS

* Universal Algebra
- P. Cohn.
Universal Algebra, Harper & Row, 1965.
# One of the standard textbook.

- W. Wechler.
Universal algebra for computer scientists. Springer-Verlag, 1992.
# Universal algebras, equational logic and rewriting are mentioned.
# Suitable for rewriting theoretists.

* Category Theory
- R.L. Crole.
Categories for Types, Cambridge Mathematical Textbook,1993.	
# The first chapter contains introduction to basic category theory.