{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T11:02:12Z","timestamp":1740135732255,"version":"3.37.3"},"reference-count":40,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2017,8,22]],"date-time":"2017-08-22T00:00:00Z","timestamp":1503360000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Constraint handling rules provide descriptions for constraint solvers. However, they fall short when those constraints specify some binding structure, like higher-rank types in a constraint-based type inference algorithm. In this paper, the term syntax of constraints is replaced by \u03bb-tree syntax, in which binding is explicit, and a new \u2207 generic quantifier is introduced, which is used to create new fresh constants.<\/jats:p>","DOI":"10.1017\/s1471068417000230","type":"journal-article","created":{"date-parts":[[2017,8,22]],"date-time":"2017-08-22T08:14:30Z","timestamp":1503389670000},"page":"992-1009","source":"Crossref","is-referenced-by-count":0,"title":["Constraint handling rules with binders, patterns and generic quantification"],"prefix":"10.1017","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5429-7589","authenticated-orcid":false,"given":"ALEJANDRO","family":"SERRANO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JURRIAAN","family":"HAGE","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2017,8,22]]},"reference":[{"key":"S1471068417000230_ref18","doi-asserted-by":"crossref","unstructured":"Koninck L. , Schrijvers T. and Demoen B. 2007. User-definable rule priorities for CHR. In Proc. of International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP '07. ACM, 25\u201336.","DOI":"10.1145\/1273920.1273924"},{"key":"S1471068417000230_ref12","doi-asserted-by":"crossref","unstructured":"Eisenberg R. A. , Weirich S. and Ahmed H. G. 2016. Visible type application. In Programming Languages and Systems 25th European Symposiun on Programming \u2013 ESOP 2016, Lecture Notes in Computer Science 9632. Springer, 229\u2013254.","DOI":"10.1007\/978-3-662-49498-1_10"},{"key":"S1471068417000230_ref1","doi-asserted-by":"crossref","unstructured":"Abdennadher S. 1997. Operational semantics and confluence of constraint propagation rules. In Proc. of CP97, Linz, Austria, October 29\u2013November 1, G. Smolka , Ed.","DOI":"10.1007\/BFb0017444"},{"key":"S1471068417000230_ref36","unstructured":"Swift Team. 2016. Type checker design and implementation. Available at https:\/\/github.com\/apple\/swift\/blob\/master\/docs\/TypeChecker.rst"},{"key":"S1471068417000230_ref27","first-page":"389","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pottier","year":"2005"},{"key":"S1471068417000230_ref8","unstructured":"Dijkstra A. , van~den~Geest G. , Heeren B. and Swierstra S. D. 2007. Modelling Scoped Instances with Constraint Handling Rules. Technical Report, Department of Information and Computing Sciences, Utrecht University."},{"key":"S1471068417000230_ref34","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006137"},{"key":"S1471068417000230_ref38","unstructured":"Voets D. , Pilozzi P. and De~Schreye D. 2008. A new approach to termination analysis of constraint handling rules. In Pre-proceedings of LOPSTR 2008, pp. 28\u201342."},{"key":"S1471068417000230_ref33","first-page":"1","volume-title":"Programming Languages and Systems","author":"Stuckey","year":"2006"},{"key":"S1471068417000230_ref29","doi-asserted-by":"crossref","unstructured":"Serrano A. and Hage J. 2016. Type error diagnosis for embedded DSLs by two-stage specialized type rules. In Programming Languages and Systems 25th European Symposium on Programming \u2013 ESOP 2016, Lecture Notes in Computer Science 9632. Springer, 672\u2013698.","DOI":"10.1007\/978-3-662-49498-1_26"},{"key":"S1471068417000230_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"S1471068417000230_ref6","unstructured":"Csorba J. , Zombori Z. and Szeredi P. 2012. Pros and Cons of Using CHR for Type Inference. Unpublished, available in the first author's web page."},{"key":"S1471068417000230_ref28","doi-asserted-by":"crossref","unstructured":"Qian Z. 1993. Linear Unification of Higher-Order Patterns, 391\u2013405.","DOI":"10.1007\/3-540-56610-4_78"},{"key":"S1471068417000230_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"S1471068417000230_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609886"},{"key":"S1471068417000230_ref40","unstructured":"Wazny J. 2006. Type Inference and Type Error Diagnosis for Hindley\/Milner with Extensions. PhD Thesis, University of Melbourne, Australia."},{"key":"S1471068417000230_ref19","unstructured":"Miller D. 1990. An Extension to ML to Handle Bound Variables in Data Structures. Technical Report, Department of Computer and Information Science, University of Pennsylvania."},{"key":"S1471068417000230_ref10","doi-asserted-by":"crossref","unstructured":"Duck G. J. , Stuckey P. J. and Sulzmann M. 2007. Observable confluence for constraint handling rules. In Proc. of ICLP 2007, Porto, Portugal, September 8\u201313, 2007, V. Dahl and I. Niemel\u00e4 , Eds., 224\u2013239.","DOI":"10.1007\/978-3-540-74610-2_16"},{"key":"S1471068417000230_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.016"},{"key":"S1471068417000230_ref26","unstructured":"Pilozzi P. and De~Schreye D. 2008. Termination analysis of CHR revisited. In Proc. of ICLP 2008, Udine, Italy, December 9\u201313, M. Garcia~de~la~Banda and E. Pontelli , Eds. 501\u2013515."},{"key":"S1471068417000230_ref24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796806006034","article-title":"Practical type inference for arbitrary-rank types","volume":"17","author":"Peyton~Jones","year":"2007","journal-title":"Journal of Functional Programming"},{"key":"S1471068417000230_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068409990123"},{"key":"S1471068417000230_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"S1471068417000230_ref20","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"S1471068417000230_ref35","doi-asserted-by":"crossref","unstructured":"Sulzmann M. , Wazny J. and Stuckey P. J. 2006. A framework for extended algebraic data types. In Proc. of International Symposium on Functional and Logic Programming, FLOPS '06, 47\u201364.","DOI":"10.1007\/11737414_5"},{"key":"S1471068417000230_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.03.021"},{"key":"S1471068417000230_ref2","doi-asserted-by":"crossref","unstructured":"Abdennadher S. and Sch\u00fctz H. 1998. CHR\u2228: A flexible query language. In Proc. of International Conference on Flexible Query Answering Systems, FQAS '98, 1\u201314.","DOI":"10.1007\/BFb0055987"},{"key":"S1471068417000230_ref3","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"S1471068417000230_ref25","doi-asserted-by":"crossref","unstructured":"Pfenning F. and Elliott C. 1988. Higher-order abstract syntax. In Proc. of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation, PLDI '88. ACM, New York, 199\u2013208.","DOI":"10.1145\/53990.54010"},{"key":"S1471068417000230_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"S1471068417000230_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326"},{"key":"S1471068417000230_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"S1471068417000230_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1462166.1462169"},{"key":"S1471068417000230_ref9","doi-asserted-by":"crossref","unstructured":"Duck G. J. , Stuckey P. J. , de~la~Banda M. G. and Holzbaur C. 2004. The refined operational semantics of constraint handling rules. In Proc. of ICLP 2004, Saint-Malo, France, September 6\u201310, 90\u2013104.","DOI":"10.1007\/978-3-540-27775-0_7"},{"key":"S1471068417000230_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S1471068417000230_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_16"},{"key":"S1471068417000230_ref39","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000098"},{"key":"S1471068417000230_ref30","doi-asserted-by":"crossref","unstructured":"Shinwell M. R. , Pitts A. M. and Gabbay M. J. 2003. FreshML: Programming with binders made simple. In Proc. of ACM SIGPLAN International Conference on Functional Programming, ICFP '03. ACM, 263\u2013274.","DOI":"10.1145\/944705.944729"},{"key":"S1471068417000230_ref11","doi-asserted-by":"crossref","unstructured":"Dunfield J. and Krishnaswami N. R. 2013. Complete and easy bidirectional typechecking for higher-rank polymorphism. In Proc. of International Conference on Functional Programming, ICFP'13, G. Morrisett and T. Uustalu , Eds. ACM, 429\u2013442.","DOI":"10.1145\/2500365.2500582"},{"key":"S1471068417000230_ref14","first-page":"298","volume-title":"Proving Termination of Constraint Solver Programs","author":"Fr\u00fchwirth","year":"2000"}],"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\/S1471068417000230","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T21:54:52Z","timestamp":1555451692000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068417000230\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,22]]},"references-count":40,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["S1471068417000230"],"URL":"https:\/\/doi.org\/10.1017\/s1471068417000230","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2017,8,22]]}}}