{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:09:56Z","timestamp":1743023396008,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030590246"},{"type":"electronic","value":"9783030590253"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-59025-3_1","type":"book-chapter","created":{"date-parts":[[2020,9,10]],"date-time":"2020-09-10T07:06:21Z","timestamp":1599721581000},"page":"3-9","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and\u00a0SOL"],"prefix":"10.1007","author":[{"given":"Makoto","family":"Hamana","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,2]]},"reference":[{"unstructured":"Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)","key":"1_CR1"},{"doi-asserted-by":"crossref","unstructured":"Arkor, N., Fiore, M.: Algebraic models of simple type theories: a polynomial approach. In: Proceedings of LICS 2020, pp. 88\u2013101. ACM (2020)","key":"1_CR2","DOI":"10.1145\/3373718.3394771"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10721975_4","volume-title":"Rewriting Techniques and Applications","author":"F Blanqui","year":"2000","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 47\u201361. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10721975_4"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.tcs.2015.07.045","volume":"611","author":"F Blanqui","year":"2016","unstructured":"Blanqui, F.: Termination of rewrite relations on $$\\lambda $$-terms based on Girard\u2019s notion of reducibility. Theor. Comput. Sci. 611, 50\u201386 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"1_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"},{"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)","key":"1_CR6","DOI":"10.1109\/LICS.2013.59"},{"doi-asserted-by":"crossref","unstructured":"Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of PPDP 2002, pp. 26\u201337. ACM Press (2002)","key":"1_CR7","DOI":"10.1145\/571157.571161"},{"doi-asserted-by":"crossref","unstructured":"Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proceedings of LICS 2008, pp. 57\u201368 (2008)","key":"1_CR8","DOI":"10.1109\/LICS.2008.38"},{"key":"1_CR9","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"},{"unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings of LICS 1999, pp. 193\u2013202 (1999)","key":"1_CR10"},{"doi-asserted-by":"crossref","unstructured":"Fiore, M., Staton, S.: Substitution, jumps, and algebraic effects. In: Proceedings of the CSL-LICS 2014, pp. 41:1\u201341:10 (2014)","key":"1_CR11","DOI":"10.1145\/2603088.2603163"},{"doi-asserted-by":"crossref","unstructured":"Hamana, M., Abe, T., Kikuchi, K.: Polymorphic computation systems: theory and practice of confluence with call-by-value. Sci. Comput. Program. 187(102322) (2020)","key":"1_CR12","DOI":"10.1016\/j.scico.2019.102322"},{"key":"1_CR13","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 $$-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":"1_CR14","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"},{"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)","key":"1_CR15","DOI":"10.1145\/1273920.1273933"},{"doi-asserted-by":"crossref","unstructured":"Hamana, M.: Initial algebra semantics for cyclic sharing tree structures. Log. Methods Comput. Sci. 6(3(15)), 1\u20131\u201323 (2010)","key":"1_CR16","DOI":"10.2168\/LMCS-6(3:15)2010"},{"key":"1_CR17","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":"1_CR18","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"},{"key":"1_CR19","first-page":"1","volume":"13","author":"M Hamana","year":"2017","unstructured":"Hamana, M.: Cyclic datatypes modulo bisimulation based on second-order algebraic theories. Log. Methods Comput. Sci. 13, 1\u201338 (2017)","journal-title":"Log. Methods Comput. Sci."},{"issue":"22","key":"1_CR20","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."},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-90686-7_7","volume-title":"Functional and Logic Programming","author":"M Hamana","year":"2018","unstructured":"Hamana, M.: Polymorphic rewrite rules: confluence, type inference, and instance validation. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 99\u2013115. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-90686-7_7"},{"doi-asserted-by":"crossref","unstructured":"Hamana, M.: How to prove decidability of equational theories with second-order computation analyser SOL. J. Funct. Program. 29(e20) (2019)","key":"1_CR22","DOI":"10.1017\/S0956796819000157"},{"unstructured":"Hamana, M.: Modular termination for second-order computation rules and application to algebraic effect handlers. arXiv:1912.03434 (2020)","key":"1_CR23"},{"unstructured":"Klop, J.W.: Combinatory reduction systems. Ph.D. thesis, CWI. Mathematical Centre Tracts, vol. 127, Amsterdam (1980)","key":"1_CR24"},{"doi-asserted-by":"crossref","unstructured":"Staton, S.: An algebraic presentation of predicate logic. In: Proceedings of FOSSACS 201, pp. 401\u2013417 (2013)","key":"1_CR25","DOI":"10.1007\/978-3-642-37075-5_26"},{"doi-asserted-by":"crossref","unstructured":"Staton, S.: Instances of computational effects: an algebraic perspective. In: Proceedings of LICS 2013, p. 519 (2013)","key":"1_CR26","DOI":"10.1109\/LICS.2013.58"},{"doi-asserted-by":"crossref","unstructured":"Staton, S.: Algebraic effects, linearity, and quantum programming languages. In: Proceedings of POPL 2015, pp. 395\u2013406 (2015)","key":"1_CR27","DOI":"10.1145\/2775051.2676999"},{"issue":"6","key":"1_CR28","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/j.ipl.2003.12.008","volume":"89","author":"T Yokoyama","year":"2004","unstructured":"Yokoyama, T., Hu, Z., Takeichi, M.: Deterministic second-order patterns. Inf. Process. Lett. 89(6), 309\u2013314 (2004)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59025-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T14:25:37Z","timestamp":1619274337000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-59025-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030590246","9783030590253"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59025-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"2 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FLOPS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Functional and Logic Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Akita","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"flops2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.ipl.riec.tohoku.ac.jp\/FLOPS2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4.1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}