{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T20:24:23Z","timestamp":1768163063494,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T00:00:00Z","timestamp":1725840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,9]]},"DOI":"10.1145\/3678232.3678233","type":"proceedings-article","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:17Z","timestamp":1725489317000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Higher-Order unification for free!: Reusing the meta-language unification for the object language"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-5934-8776","authenticated-orcid":false,"given":"Davide","family":"Fissore","sequence":"first","affiliation":[{"name":"Inria - Universit\u00e9 C\u00f4te d'Azur, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7783-528X","authenticated-orcid":false,"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[{"name":"Inria - Universit\u00e9 C\u00f4te d'Azur, France"}]}],"member":"320","published-online":{"date-parts":[[2024,9,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Andreas Abel and Brigitte Pientka. 2018. Extensions to Miller\u2019s Pattern Unification for Dependent Types and Records. https:\/\/api.semanticscholar.org\/CorpusID:51885863"},{"key":"e_1_3_2_1_2_1","volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287584"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012823"},{"key":"e_1_3_2_1_6_1","volume-title":"The Coq Workshop","author":"Fissore Davide","year":"2023","unstructured":"Davide Fissore and Enrico Tassi. 2023. A new Type-Class solver for Coq in Elpi. In The Coq Workshop 2023. Bialystok, Poland. https:\/\/inria.hal.science\/hal-04467855"},{"key":"e_1_3_2_1_7_1","unstructured":"Thom Fruehwirth. 2017. Constraint Handling Rules - What Else?arxiv:1701.02668\u00a0[cs.PL]"},{"key":"e_1_3_2_1_8_1","unstructured":"Andrew Gacek. 2008. The Abella Interactive Theorem Prover (System Description). arxiv:0803.2305\u00a0[cs.LO]"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575683"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000427"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_13_1","unstructured":"Spiro Michaylov and Frank Pfenning. 1993. Higher-Order Logic Programming as Constraint Logic Programming. In Principles and Practice of Constraint Programming. https:\/\/api.semanticscholar.org\/CorpusID:9980455"},{"key":"e_1_3_2_1_14_1","volume-title":"Extensions of Logic Programming, Peter Schroeder-Heister (Ed.)","author":"Miller Dale","unstructured":"Dale Miller. 1991. A logic programming language with lambda-abstraction, function variables, and simple unification. In Extensions of Logic Programming, Peter Schroeder-Heister (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 253\u2013281."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"e_1_3_2_1_17_1","volume-title":"The Metalanguage \u03bb prolog and Its Implementation","author":"Nadathur Gopalan","unstructured":"Gopalan Nadathur. 2001. The Metalanguage \u03bb prolog and Its Implementation. In Functional and Logic Programming, Herbert Kuchen and Kazunori Ueda (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1\u201320."},{"key":"e_1_3_2_1_18_1","unstructured":"Gopalan Nadathur and Dale Miller. 1988. An Overview of Lambda-Prolog. 810\u2013827."},{"key":"e_1_3_2_1_19_1","volume-title":"Vol.\u00a02283","author":"Nipkow Tobias","unstructured":"Tobias Nipkow, Lawrence\u00a0C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, Vol.\u00a02283. Springer."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881873"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39186"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_23_1","volume-title":"System Description: Twelf \u2014 A Meta-Logical Framework for Deductive Systems. In Automated Deduction \u2014 CADE-16","author":"Pfenning Frank","year":"1999","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. 1999. System Description: Twelf \u2014 A Meta-Logical Framework for Deductive Systems. In Automated Deduction \u2014 CADE-16. Springer Berlin Heidelberg, Berlin, Heidelberg, 202\u2013206."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_1_25_1","volume-title":"Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","author":"Sozeau Matthieu","unstructured":"Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278\u2013293."},{"key":"e_1_3_2_1_26_1","volume-title":"The Fourth International Workshop on Coq for Programming Languages","author":"Tassi Enrico","year":"2018","unstructured":"Enrico Tassi. 2018. Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi \u03bb Prolog dialect). In The Fourth International Workshop on Coq for Programming Languages. Los Angeles, CA, United States. https:\/\/inria.hal.science\/hal-01637063"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CVIT.2016.23"},{"key":"e_1_3_2_1_28_1","unstructured":"The Coq Development Team. 2023. The Coq Reference Manual \u2013 Release 8.18.0. https:\/\/coq.inria.fr\/doc\/V8.18.0\/refman."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_3_2_1_30_1","volume-title":"Theorem Proving in Higher Order Logics, Elsa\u00a0L","author":"Wenzel Markus","unstructured":"Markus Wenzel. 1997. Type classes and overloading in higher-order logic. In Theorem Proving in Higher Order Logics, Elsa\u00a0L. Gunter and Amy Felty (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 307\u2013322."},{"key":"e_1_3_2_1_31_1","volume-title":"Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","author":"Wenzel Makarius","unstructured":"Makarius Wenzel, Lawrence\u00a0C. Paulson, and Tobias Nipkow. 2008. The Isabelle Framework. In Theorem Proving in Higher Order Logics, Otmane\u00a0Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 33\u201338."}],"event":{"name":"PPDP 2024: 26th International Symposium on Principles and Practice of Declarative Programming","location":"Milano Italy","acronym":"PPDP 2024"},"container-title":["Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678232.3678233","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3678232.3678233","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:09Z","timestamp":1750287249000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678232.3678233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,9]]},"references-count":31,"alternative-id":["10.1145\/3678232.3678233","10.1145\/3678232"],"URL":"https:\/\/doi.org\/10.1145\/3678232.3678233","relation":{},"subject":[],"published":{"date-parts":[[2024,9,9]]},"assertion":[{"value":"2024-09-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}