{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T19:54:15Z","timestamp":1768161255156,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032159809","type":"print"},{"value":"9783032159816","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15981-6_5","type":"book-chapter","created":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T17:13:27Z","timestamp":1768151607000},"page":"77-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Determinacy Checking for\u00a0Elpi: an\u00a0Higher-Order Logic Programming Language with\u00a0Cut"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-5934-8776","authenticated-orcid":false,"given":"Davide","family":"Fissore","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7783-528X","authenticated-orcid":false,"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,12]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Blot, V., et al.: Compositional pre-processing for automated reasoning in dependent type theory. In: Krebbers, R., Traytel, D., Pientka, B., Zdancewic, S. (eds.) Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, 16\u201317 January 2023, pp. 63\u201377. ACM (2023). https:\/\/doi.org\/10.1145\/3573105.3575676","DOI":"10.1145\/3573105.3575676"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"de\u00a0Bruin, A., de\u00a0Vink, E.P.: Continuation semantics for prolog with cut. In: D\u00edaz, J., Orejas, F. (eds.) TAPSOFT \u201989, pp. 178\u2013192. Springer, Heidelberg (1989). ISBN 978-3-540-46116-6","DOI":"10.1007\/3-540-50939-9_132"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Cohen, C., Crance, E., Mahboubi, A.: Trocq: proof transfer for free, with or without univalence. In: Weirich, S. (ed.) Programming Languages and Systems, pp. 239\u2013268. Springer, Cham (2024). ISBN 978-3-031-57262-3","DOI":"10.1007\/978-3-031-57262-3_10"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy builder: algebraic hierarchies made easy in coq with elpi. In: Proceedings of FSCD, LIPIcs, vol. 167, pp. 34:1\u201334:21 (2020), ISBN 978-3-95977-155-9. ISSN 1868-8969. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.34. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2020.34","DOI":"10.4230\/LIPIcs.FSCD.2020.34"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Debray, S.K., Warren, D.S.: Functional computations in logic programs, vol.\u00a011, p. 451\u2013481. Association for Computing Machinery (1989). ISSN 0164-0925. https:\/\/doi.org\/10.1145\/65979.65984","DOI":"10.1145\/65979.65984"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$Prolog interpreter. In: Proceedings of LPAR, LNCS, vol. 9450, pp. 460\u2013468. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32. https:\/\/inria.hal.science\/hal-01176856v1","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"5_CR7","unstructured":"Fissore, D.: Elpi formalization (2025). https:\/\/github.com\/gares\/elpi-formalization"},{"key":"5_CR8","unstructured":"Fissore, D., Tassi, E.: A new type-class solver for coq in elpi. In: The Coq Workshop (2023). https:\/\/inria.hal.science\/hal-04467855"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Fissore, D., Tassi, E.: Higher-order unification for free!: reusing the meta-language unification for the object language. In: Proceedings of PPDP, pp. 1\u201313. ACM (2024). ISBN 9798400709692. https:\/\/doi.org\/10.1145\/3678232.3678233","DOI":"10.1145\/3678232.3678233"},{"key":"5_CR10","unstructured":"Fissore, D., Tassi, E.: Determinacy Checking for Elpi: an Higher-Order Logic Programming language with Cut (2025). https:\/\/inria.hal.science\/hal-05026472"},{"key":"5_CR11","unstructured":"Gonthier, G.: A computer-checked proof of the Four Color Theorem. Technical report, Inria (2023). https:\/\/inria.hal.science\/hal-04034866"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, 22\u201326 July 2013. Proceedings, Lecture Notes in Computer Science, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013), https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14. https:\/\/inria.hal.science\/hal-00816699v1","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire, B., L\u00e9chenet, J.C., Tassi, E.: Practical and sound equality tests, automatically. In: Proceedings of CPP, pp. 167\u2013181. Association for Computing Machinery (2023). ISBN 9798400700262. https:\/\/doi.org\/10.1145\/3573105.3575683","DOI":"10.1145\/3573105.3575683"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Guidi, F., Coen, C.S., Tassi, E.: Implementing type theory in higher order constraint logic programming. In: Mathematical Structures in Computer Science, vol.\u00a029, pp. 1125\u20131150. Cambridge University Press (2019). https:\/\/doi.org\/10.1017\/S0960129518000427","DOI":"10.1017\/S0960129518000427"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Hanus, M., Prott, K.O.: Determinism Types for Functional Logic Programming. In: Proceedings of PPDP, pp. 47\u201359 (2025)","DOI":"10.1145\/3756907.3756915"},{"key":"5_CR16","unstructured":"Henderson, F., Somogyi, Z., Conway, T.: Determinism analysis in the mercury compiler. In: Proceedings of Australian Computer Science Conference, pp. 337\u2013346 (1996)"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Krebbers, R., van\u00a0der Maas, L., Tassi, E.: Inductive predicates via least fixpoints in higher-order separation logic. In: Forster, Y., Keller, C. (eds.) 16th International Conference on Interactive Theorem Proving (ITP 2025), Leibniz International Proceedings in Informatics (LIPIcs), vol. 352, pp. 27:1\u201327:21. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2025). ISBN 978-3-95977-396-6. ISSN 1868-8969. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2025.27. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2025.27","DOI":"10.4230\/LIPIcs.ITP.2025.27"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Kriener, J., King, A.: Redalert: Determinacy Inference for Prolog, vol.\u00a011, pp. 537\u2013553. Cambridge University Press, Cambridge (2011)","DOI":"10.1017\/S1471068411000160"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"L\u00f3pez-Garc\u00eda, P., Bueno, F., Hermenegildo, M.: Determinacy analysis for logic programs using mode and type information. In: Etalle, S. (ed.) Logic Based Program Synthesis and Transformation, pp. 19\u201335. Springer, Heidelberg (2005). ISBN 978-3-540-31683-1","DOI":"10.1007\/11506676_2"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"van\u00a0der Maas, L.: Extending the Iris Proof Mode with Inductive Predicates using Elpi. Master\u2019s thesis, Radboud University Nijmegen (2024). https:\/\/doi.org\/10.5281\/zenodo.12568604","DOI":"10.5281\/zenodo.12568604"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Mahboubi, A., Tassi, E.: Mathematical Components. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.7118596","DOI":"10.5281\/zenodo.7118596"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Extensions of Logic Programming, pp. 253\u2013281. Springer, Heidelberg (1991). ISBN 978-3-540-46879-0","DOI":"10.1007\/BFb0038698"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)","DOI":"10.1017\/CBO9781139021326"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/s10817-018-9483-3","volume":"63","author":"DA Miller","year":"2018","unstructured":"Miller, D.A.: Mechanized metatheory revisited. J. Autom. Reason. 63, 625\u2013665 (2018)","journal-title":"J. Autom. Reason."},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Nakamura, K.: Control of logic program execution based on the functional relations. In: Proceedings of ICLP, pp. 505\u2013512. Springer, Heidelberg (1986). ISBN 3540164928","DOI":"10.1007\/3-540-16492-8_98"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of PLDI, pp. 199\u2013208. Association for Computing Machinery (1988). ISBN 0897912691. https:\/\/doi.org\/10.1145\/53990.54010","DOI":"10.1145\/53990.54010"},{"key":"5_CR27","unstructured":"Qi, X.: An Implementation of the Language Lambda Prolog Organized around Higher-Order Pattern Unification. Ph.D. thesis, Graduate School of the University of Minnesota (2009). https:\/\/arxiv.org\/abs\/0911.5203"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Somogyi, Z., Henderson, F., Conway, T.: The execution algorithm of mercury, an efficient purely declarative logic programming language, vol.\u00a029, pp. 17\u201364 (1996). ISSN 0743-1066. https:\/\/doi.org\/10.1016\/S0743-1066(96)00068-4. https:\/\/www.sciencedirect.com\/science\/inproceedings\/pii\/S0743106696000684","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"5_CR29","unstructured":"Tassi, E.: Elpi: an extension language for Coq (Metaprogramming Coq in the Elpi $$\\lambda $$Prolog dialect). In: The Fourth International Workshop on Coq for Programming Languages (2018). https:\/\/inria.hal.science\/hal-01637063"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Tassi, E.: Deriving proved equality tests in Coq-Elpi. In: Proceedings of ITP, LIPIcs, vol. 141, pp. 29:1\u201329:18 (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CVIT.2016.23. https:\/\/inria.hal.science\/hal-01897468","DOI":"10.4230\/LIPIcs.CVIT.2016.23"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Zhou, N.f.: The language features and architecture of b-prolog. Theory Pract. Log. Program. 12(1\u20132), 189\u2013218 (2012), ISSN 1471-0684. https:\/\/doi.org\/10.1017\/S1471068411000445","DOI":"10.1017\/S1471068411000445"}],"container-title":["Lecture Notes in Computer Science","Practical Aspects of Declarative Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15981-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T17:13:30Z","timestamp":1768151610000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15981-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032159809","9783032159816"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15981-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PADL","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Practical Aspects of Declarative Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"padl2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl26.sigplan.org\/home\/PADL-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}