{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:11Z","timestamp":1759638911483,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,7,14]],"date-time":"2007-07-14T00:00:00Z","timestamp":1184371200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2007,7,14]]},"DOI":"10.1145\/1273920.1273933","type":"proceedings-article","created":{"date-parts":[[2012,10,10]],"date-time":"2012-10-10T14:45:29Z","timestamp":1349880329000},"page":"97-108","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Higher-order semantic labelling for inductive datatype systems"],"prefix":"10.1145","author":[{"given":"Makoto","family":"Hamana","sequence":"first","affiliation":[{"name":"Gunma University \/ The University of Tokyo"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,7,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/10721975_4","volume-title":"Rewriting Techniques and Application (RTA","author":"Blanqui F.","year":"2000","unstructured":"F. Blanqui . Termination and confluence of higher-order rewrite systems . In Rewriting Techniques and Application (RTA 2000 ), LNCS 1833, pages 47 -- 61 . Springer , 2000. F. Blanqui. Termination and confluence of higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833, pages 47--61. Springer, 2000."},{"key":"e_1_3_2_1_2_1","volume-title":"INRIA","author":"Blanqui F.","year":"2006","unstructured":"F. Blanqui . (HO) RPO revisited. Technical Report 5972 , INRIA , 2006 . Research report. F. Blanqui. (HO)RPO revisited. Technical Report 5972, INRIA, 2006. Research report."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00347-9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00183-7"},{"key":"e_1_3_2_1_5_1","first-page":"62","volume-title":"CSN-95: Computer Science in the Netherlands","author":"Bloo R.","year":"1995","unstructured":"R. Bloo and K. H. Rose . Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection . In CSN-95: Computer Science in the Netherlands , pages 62 -- 72 , 1995 . R. Bloo and K. H. Rose. Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In CSN-95: Computer Science in the Netherlands, pages 62--72, 1995."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/645710.664465"},{"key":"e_1_3_2_1_7_1","first-page":"459","volume-title":"Handbook of Theoretical Computer Science","author":"Courcelle B.","year":"1990","unstructured":"B. Courcelle . Recursive application schemes. In J. van Leeuwen, editor , Handbook of Theoretical Computer Science , pages 459 -- 492 . 1990 . Chapter 9 , vol. B. B. Courcelle. Recursive application schemes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 459--492. 1990. Chapter 9, vol. B."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671587"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788948"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8748-4"},{"key":"e_1_3_2_1_13_1","first-page":"348","volume-title":"Asian Symposium on Programming Languages and Systems (APLAS 2004","author":"Hamana M.","year":"2004","unstructured":"M. Hamana . Free S-monoids : A higher-order syntax with metavariables . In Asian Symposium on Programming Languages and Systems (APLAS 2004 ), LNCS 3302, pages 348 -- 363 , 2004 . M. Hamana. Free S-monoids: A higher-order syntax with metavariables. In Asian Symposium on Programming Languages and Systems (APLAS 2004), LNCS 3302, pages 348--363, 2004."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_11"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003821"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788974"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_29"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1206035.1206037"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_70"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0002"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.09.004"},{"key":"e_1_3_2_1_24_1","first-page":"294","volume-title":"6th International Conference (RTA-95)","author":"Lescanne P.","year":"1995","unstructured":"P. Lescanne and J. Rouyer-Degli . Explicit substitutions with de Bruijn's levels. In Rewriting Techniques and Applications , 6th International Conference (RTA-95) , LNCS 914, pages 294 -- 308 . Springer , 1995 . P. Lescanne and J. Rouyer-Degli. Explicit substitutions with de Bruijn's levels. In Rewriting Techniques and Applications, 6th International Conference (RTA-95), LNCS 914, pages 294--308. Springer, 1995."},{"key":"e_1_3_2_1_25_1","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician","author":"Lane S. Mac","year":"1971","unstructured":"S. Mac Lane . Categories for the Working Mathematician , volume 5 of Graduate Texts in Mathematics . Springer-Verlag , New York , 1971 . S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888269"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/648232.753126"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151658"},{"key":"e_1_3_2_1_30_1","volume-title":"Draft","author":"van Oostrom V.","year":"2005","unstructured":"V. van Oostrom . Counterexamples to higher-order modularity . Draft , 2005 . V. van Oostrom. Counterexamples to higher-order modularity. Draft, 2005."},{"key":"e_1_3_2_1_31_1","first-page":"305","volume-title":"the First International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA '93)","author":"van de Pol J.","year":"1994","unstructured":"J. van de Pol . Termination proofs for higher-order rewrite systems . In the First International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA '93) , LNCS 816, pages 305 -- 325 , 1994 . J. van de Pol. Termination proofs for higher-order rewrite systems. In the First International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA '93), LNCS 816, pages 305--325, 1994."},{"key":"e_1_3_2_1_32_1","first-page":"261","volume-title":"12th International Conference (RTA 2001","author":"van Raamsdonk F.","year":"2001","unstructured":"F. van Raamsdonk . On termination of higher-order rewriting. In Rewriting Techniques and Applications , 12th International Conference (RTA 2001 ), pages 261 -- 275 , 2001 . F. van Raamsdonk. On termination of higher-order rewriting. In Rewriting Techniques and Applications, 12th International Conference (RTA 2001), pages 261--275, 2001."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088457"},{"volume-title":"Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science","year":"2003","key":"e_1_3_2_1_34_1","unstructured":"Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science . Cambridge University Press , 2003 . Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2428096.2428100"}],"event":{"name":"PPDP07: Principles and Practice of Declarative Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Wroclaw Poland","acronym":"PPDP07"},"container-title":["Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1273920.1273933","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1273920.1273933","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:58:09Z","timestamp":1750258689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1273920.1273933"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,14]]},"references-count":33,"alternative-id":["10.1145\/1273920.1273933","10.1145\/1273920"],"URL":"https:\/\/doi.org\/10.1145\/1273920.1273933","relation":{},"subject":[],"published":{"date-parts":[[2007,7,14]]},"assertion":[{"value":"2007-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}