{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T13:00:28Z","timestamp":1761310828796,"version":"build-2065373602"},"reference-count":20,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T00:00:00Z","timestamp":1757376000000},"content-version":"unspecified","delay-in-days":70,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2025,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Higher-order constructs enable more expressive and concise code by allowing procedures to be parameterized by other procedures. Assertions allow expressing partial program specifications, which can be verified either at compile time (statically) or run time (dynamically). In higher-order programs, assertions can also describe higher-order arguments. While in the context of (constraint) logic programming ((C)LP), run-time verification of higher-order assertions has received some attention, compile-time verification remains relatively unexplored. We propose a novel approach for statically verifying higher-order (C)LP programs with higher-order assertions. Although we use the\n                    <jats:sans-serif>Ciao<\/jats:sans-serif>\n                    assertion language for illustration, our approach is quite general, and we believe is applicable to similar contexts. Higher-order arguments are described using predicate properties \u2013 a special kind of property which exploits the (\n                    <jats:sans-serif>Ciao<\/jats:sans-serif>\n                    ) assertion language. We refine the syntax and semantics of these properties and introduce an abstract criterion to determine conformance to a predicate property at compile time, based on a semantic order relation comparing the predicate property with the predicate assertions. We then show how to handle these properties using an abstract interpretation-based static analyzer for programs with first-order assertions by reducing predicate properties to first-order properties. Finally, we report on a prototype implementation and evaluate it through various examples within the\n                    <jats:sans-serif>Ciao<\/jats:sans-serif>\n                    system.\n                  <\/jats:p>","DOI":"10.1017\/s147106842510015x","type":"journal-article","created":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T02:57:20Z","timestamp":1757386640000},"page":"612-630","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Hiord\n$^{{\\kern2pt}\\sharp}$\n: An Approach to the Specification and Verification of Higher-Order (C)LP Programs"],"prefix":"10.1017","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8821-0587","authenticated-orcid":false,"given":"MARCO","family":"CICCAL\u00c8","sequence":"first","affiliation":[{"name":"IMDEA Software Institute"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6215-1080","authenticated-orcid":false,"given":"DANIEL","family":"JURJO-RIVAS","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9782-8135","authenticated-orcid":false,"given":"JOSE F.","family":"MORALES","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1092-2071","authenticated-orcid":false,"given":"PEDRO","family":"L\u00d3PEZ-GARC\u00cdA","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7583-323X","authenticated-orcid":false,"given":"MANUEL V.","family":"HERMENEGILDO","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute"}]}],"member":"56","published-online":{"date-parts":[[2025,9,9]]},"reference":[{"key":"S147106842510015X_ref14","first-page":"273","volume-title":"Proc. of LOPSTR\u201999","volume":"1817","author":"Puebla","year":"2000"},{"key":"S147106842510015X_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"S147106842510015X_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068421000430"},{"key":"S147106842510015X_ref19","first-page":"225","volume-title":"PPDP\u201914","author":"Stulova","year":"2014"},{"key":"S147106842510015X_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068422000102"},{"volume-title":"The Goedel Programming Language","year":"1994","author":"Hill","key":"S147106842510015X_ref9"},{"key":"S147106842510015X_ref3","first-page":"431","volume-title":"Formal Description of Programming Concepts","author":"Cardelli","year":"1989"},{"key":"S147106842510015X_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"S147106842510015X_ref5","first-page":"48","volume-title":"1997 International Conference on Logic Programming","author":"Debray","year":"1997"},{"key":"S147106842510015X_ref16","unstructured":"Siek, J. G. and Taha, W. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 81\u201392. University of Chicago Department of Computer Science."},{"key":"S147106842510015X_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90035-2"},{"key":"S147106842510015X_ref11","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"S147106842510015X_ref4","first-page":"238","volume-title":"Proc. of POPL\u201977","author":"Cousot","year":"1977"},{"key":"S147106842510015X_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60085-2_7"},{"key":"S147106842510015X_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00068-4"},{"key":"S147106842510015X_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.12.006"},{"key":"S147106842510015X_ref2","first-page":"93","volume-title":"ASIAN\u201904","volume":"3321","author":"Cabeza","year":"2004"},{"key":"S147106842510015X_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/10722311_2"},{"key":"S147106842510015X_ref1","unstructured":"Marlow, S. 2010. Haskell 2010 language report .\u00a0Haskell Language Committee."},{"key":"S147106842510015X_ref20","first-page":"102","volume-title":"SAS\u201902","volume":"2477","author":"Vaucheret","year":"2002"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S147106842510015X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T12:56:33Z","timestamp":1761310593000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S147106842510015X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7]]},"references-count":20,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,7]]}},"alternative-id":["S147106842510015X"],"URL":"https:\/\/doi.org\/10.1017\/s147106842510015x","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2025,7]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}