Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and SOL.
An invited talk
at 15th International Symposium on Functional and Logic Programming (FLOPS'20), presented on 8, September, 2020.
SOL system (web interface)
is available. You can try confluence and termination checking of
higher-order computation by SOL at the web.
Polymorphic computation systems: Theory and practice of confluence
(with Tatsuya Abe and Kentaro Kikuchi),
Science of Computer Programming, Elsevier, Volume 187, 15 February 2020, 102322.
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.
Paper in CambridgeCore.
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.
Paper in DROPS
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).
PolySOL (web interface)
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.
(with $B>>ED(B $B0l9'(B, $B8U(B $B?69>(B, $BCfLn(B $B7=2p(B, $BIp;T(B $B@5?M(B)
$B%3%s%T%e!<%?%=%U%H%&%'%"(B, Vol. 26, No. 2, pp. 56-75, 2009.
Available: Paper in J-STAGE
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 (FLOPS'96), World Scientific, Singapore, pp. 194-209, 1996.
Abstract: English, Japanese
Available: DVI, PS,PDF
$B%3%s%T%e!<%?%=%U%H%&%'%"(B, Vol. 14, No. 6, pp. 29-43, $B4dGH=qE9(B, 1997.
Available: Paper in J-STAGE
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 @)