{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:26:35Z","timestamp":1759638395915},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319906850"},{"type":"electronic","value":"9783319906867"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-90686-7_7","type":"book-chapter","created":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T13:49:55Z","timestamp":1524491395000},"page":"99-115","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation"],"prefix":"10.1007","author":[{"given":"Makoto","family":"Hamana","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,24]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"7_CR2","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of POPL 1982, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Fiore, M., Hamana, M.: Multiversal polymorphic algebraic theories: syntax, semantics, translations, and equational logic. In: 28th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2013, pp. 520\u2013529 (2013)","DOI":"10.1109\/LICS.2013.59"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-642-15205-4_26","volume-title":"Computer Science Logic","author":"M Fiore","year":"2010","unstructured":"Fiore, M., Hur, C.-K.: Second-order equational logic (Extended Abstract). In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 320\u2013335. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_26"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-15155-2_33","volume-title":"Mathematical Foundations of Computer Science 2010","author":"M Fiore","year":"2010","unstructured":"Fiore, M., Mahmoud, O.: Second-order algebraic theories. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 368\u2013380. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15155-2_33"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-30477-7_23","volume-title":"Programming Languages and Systems","author":"M Hamana","year":"2004","unstructured":"Hamana, M.: Free $$\\Sigma $$\u03a3-monoids: a higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 348\u2013363. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30477-7_23"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-32033-3_11","volume-title":"Term Rewriting and Applications","author":"M Hamana","year":"2005","unstructured":"Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 135\u2013149. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_11"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Proceedings of PPDP 2007, pp. 97\u2013108. ACM Press (2007)","DOI":"10.1145\/1273920.1273933"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-11999-6_5","volume-title":"Functional and Constraint Logic Programming","author":"M Hamana","year":"2010","unstructured":"Hamana, M.: Semantic labelling for proving termination of combinatory reduction systems. In: Escobar, S. (ed.) WFLP 2009. LNCS, vol. 5979, pp. 62\u201378. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11999-6_5"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-19805-2_26","volume-title":"Foundations of Software Science and Computational Structures","author":"M Hamana","year":"2011","unstructured":"Hamana, M.: Polymorphic abstract syntax via grothendieck construction. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 381\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_26"},{"issue":"22","key":"7_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110266","volume":"1","author":"M Hamana","year":"2017","unstructured":"Hamana, M.: How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. Proc. ACM Program. Lang. 1(22), 1\u201328 (2017)","journal-title":"Proc. ACM Program. Lang."},{"issue":"4","key":"7_CR13","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980)","journal-title":"J. ACM"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/1206035.1206037","volume":"54","author":"J-P Jouannaud","year":"2007","unstructured":"Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. J. ACM 54(1), 2:1\u20132:48 (2007)","journal-title":"J. ACM"},{"issue":"2","key":"7_CR15","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/2699913","volume":"16","author":"J-P Jouannaud","year":"2015","unstructured":"Jouannaud, J.-P., Rubio, A.: Normal higher-order termination. ACM Trans. Comput. Log. 16(2), 13:1\u201313:38 (2015)","journal-title":"ACM Trans. Comput. Log."},{"key":"7_CR16","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"DONALD E. KNUTH","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Computational Problem in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Lindley, S., Stark, I.: Reducibility and $$\\top \\top $$\u22a4\u22a4 for computation types. In: Proceedings of TLCA 2005, pp. 262\u2013277 (2005)","DOI":"10.1007\/11417170_20"},{"issue":"3","key":"7_CR18","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1017\/S0956796898003037","volume":"8","author":"J Maraist","year":"1998","unstructured":"Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275\u2013317 (1998)","journal-title":"J. Funct. Program."},{"issue":"1","key":"7_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(97)00143-6","volume":"192","author":"R Mayr","year":"1998","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3\u201329 (1998)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"7_CR20","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput. 1(4), 497\u2013536 (1991)","journal-title":"J. Log. Comput."},{"key":"7_CR21","unstructured":"Moggi, E.: Computational lambda-calculus and monads. LFCS ECS-LFCS-88-66, University of Edinburgh (1988)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-319-63046-5_24","volume-title":"Automated Deduction \u2013 CADE 26","author":"J Nagele","year":"2017","unstructured":"Nagele, J., Felgenhauer, B., Middeldorp, A.: CSI: new evidence \u2013 a progress report. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 385\u2013397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_24"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proceedings of 6th IEEE Symposium Logic in Computer Science, pp. 342\u2013349 (1991)","DOI":"10.1109\/LICS.1991.151658"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11805618_13","volume-title":"Term Rewriting and Applications","author":"Y Ohta","year":"2006","unstructured":"Ohta, Y., Hasegawa, M.: A terminating and confluent linear lambda calculus. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 166\u2013180. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_13"},{"key":"7_CR25","unstructured":"Onozawa, K., Kikuchi, K., Aoto, T., Toyama, Y.: ACPH: System description. In: 6th Confluence Competition (CoCo 2017)(2017)"},{"issue":"6","key":"7_CR26","doi-asserted-by":"publisher","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A Sabry","year":"1997","unstructured":"Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Trans. Program. Lang. Syst. 19(6), 916\u2013941 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Sheard, T., Jones, S.P.: Template metaprogramming for Haskell. In: Proceedings of Haskell Workshop 2002 (2002)","DOI":"10.1145\/581690.581691"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-642-37075-5_26","volume-title":"Foundations of Software Science and Computation Structures","author":"S Staton","year":"2013","unstructured":"Staton, S.: An algebraic presentation of predicate logic. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 401\u2013417. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_26"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Staton, S.: Instances of computational effects: an algebraic perspective. In: Proceedings of LICS 2013, p. 519 (2013)","DOI":"10.1109\/LICS.2013.58"},{"issue":"1","key":"7_CR30","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1145\/2775051.2676999","volume":"50","author":"Sam Staton","year":"2015","unstructured":"Staton, S.: Algebraic effects, linearity, and quantum programming languages. In: Proceedings of POPL 2015, pp. 395\u2013406 (2015)","journal-title":"ACM SIGPLAN Notices"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90686-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,16]],"date-time":"2019-10-16T18:29:52Z","timestamp":1571250592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90686-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319906850","9783319906867"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90686-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}