{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:37Z","timestamp":1779836737053,"version":"3.53.1"},"reference-count":66,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2013,12,13]],"date-time":"2013-12-13T00:00:00Z","timestamp":1386892800000},"content-version":"unspecified","delay-in-days":42,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Correct handling of names and binders is an important issue in meta-programming. This paper presents an embedding of constraint logic programming into the \u03b1ML functional programming language, which provides a provably correct means of implementing proof search computations over inductive definitions involving names and binders modulo \u03b1-equivalence. We show that the execution of proof search in the \u03b1ML operational semantics is sound and complete with regard to the model-theoretic semantics of formulae, and develop a theory of contextual equivalence for the subclass of \u03b1ML expressions which correspond to inductive definitions and formulae. In particular, we prove that \u03b1ML expressions, which denote inductive definitions, are contextually equivalent precisely when those inductive definitions have the same model-theoretic semantics. This paper is a revised and extended version of the conference paper (Lakin, M. R. &amp; Pitts, A. M. (2009) Resolving inductive definitions with binders in higher-order typed functional programming. In\n                    <jats:italic>Proceedings of the 18th European Symposium on Programming (ESOP 2009)<\/jats:italic>\n                    , Castagna, G. (ed), Lecture Notes in Computer Science, vol. 5502. Berlin, Germany: Springer-Verlag, pp. 47\u201361) and draws on material from the first author's PhD thesis (Lakin, M. R. (2010)\n                    <jats:italic>An Executable Meta-Language for Inductive Definitions with Binders<\/jats:italic>\n                    . University of Cambridge, UK).\n                  <\/jats:p>","DOI":"10.1017\/s0956796813000245","type":"journal-article","created":{"date-parts":[[2013,12,13]],"date-time":"2013-12-13T09:55:01Z","timestamp":1386928501000},"page":"658-700","source":"Crossref","is-referenced-by-count":0,"title":["Contextual equivalence for inductive definitions with binders in higher order typed functional programming"],"prefix":"10.1017","volume":"23","author":[{"given":"MATTHEW R.","family":"LAKIN","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ANDREW M.","family":"PITTS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,12,13]]},"reference":[{"key":"S0956796813000245_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9229-y"},{"key":"S0956796813000245_ref45","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Proceedings of the 16th International Conference on Automated Deduction (CADE 1999)","author":"Pfenning","year":"1999"},{"key":"S0956796813000245_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"S0956796813000245_ref46","first-page":"15","volume-title":"Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010)","author":"Pientka","year":"2010"},{"key":"S0956796813000245_ref5","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/978-3-540-73595-3_28","volume-title":"Proceedings of the 21st International Conference on Automated Deduction (CADE 2007)","author":"Baelde","year":"2007"},{"key":"S0956796813000245_ref31","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:6)2011"},{"key":"S0956796813000245_ref22","first-page":"9","volume-title":"Proceedings of the 1997 Joint Conference on Declarative Programming (APPIA-GULP-PRODE 1997)","author":"Hanus","year":"1997"},{"key":"S0956796813000245_ref8","first-page":"104","volume-title":"Proceedings of the 19th International Workshop on Unification (UNIF 2005)","author":"Cheney","year":"2005"},{"key":"S0956796813000245_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"S0956796813000245_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_25"},{"key":"S0956796813000245_ref34","volume-title":"Relational Reasoning about Contexts","author":"Lassen","year":"1998"},{"key":"S0956796813000245_ref19","first-page":"85","volume-title":"Proceedings of the 3rd International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008)","author":"Gacek","year":"2009"},{"key":"S0956796813000245_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/173262.155113"},{"key":"S0956796813000245_ref60","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.003"},{"key":"S0956796813000245_ref44","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00115-6"},{"key":"S0956796813000245_ref6","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0956796813000245_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"S0956796813000245_ref27","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"S0956796813000245_ref21","volume-title":"Operational Equivalences for Untyped and Polymorphic Object Calculi","author":"Gordon","year":"1998"},{"key":"S0956796813000245_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836112"},{"key":"S0956796813000245_ref41","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML","author":"Milner","year":"1997"},{"key":"S0956796813000245_ref63","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S0956796813000245_ref55","first-page":"27","volume-title":"Proceedings of the 2005 ACM-SIGPLAN Workshop on ML (ML 2005)","volume":"148","author":"Pottier","year":"2006"},{"key":"S0956796813000245_ref56","unstructured":"Qi X. (2009) An Implementation of the Language \u03bbProlog Organized Around Higher-order Pattern Unification. PhD thesis, University of Minnesota."},{"key":"S0956796813000245_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"S0956796813000245_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"S0956796813000245_ref26","first-page":"26","volume-title":"Proceedings of the 1st International Static Analysis Symposium (SAS 1994)","author":"Hanus","year":"1994"},{"key":"S0956796813000245_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9220-7"},{"key":"S0956796813000245_ref24","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/BFb0056627","volume-title":"Principles of Declarative Programming (Proceedings of the Joint International Symposium PLILP\/ALP 1998)","author":"Hanus","year":"1998"},{"key":"S0956796813000245_ref35","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-540-70590-1_17","volume-title":"Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008)","author":"Levy","year":"2008"},{"key":"S0956796813000245_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.01.010"},{"key":"S0956796813000245_ref66","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/2034773.2034818","volume-title":"Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011)","author":"Weirich","year":"2011"},{"key":"S0956796813000245_ref49","first-page":"245","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts","year":"2005"},{"key":"S0956796813000245_ref59","unstructured":"Shinwell M. R. (2005) The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, University of Cambridge, UK."},{"key":"S0956796813000245_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"S0956796813000245_ref10","first-page":"269","volume-title":"Proceedings of the 20th International Conference on Logic Programming (ICLP 2004)","author":"Cheney","year":"2004"},{"key":"S0956796813000245_ref37","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"S0956796813000245_ref62","first-page":"17","article-title":"The execution algorithm of Mercury, an efficient purely declarative logic programming language.","volume":"29","author":"Somogyi","year":"1996","journal-title":"J. Funct. Program"},{"key":"S0956796813000245_ref64","first-page":"74","volume-title":"the Proceedings of the 7th International Conference on Typed Lambda Calculus and Applications (TLCA 2005)","author":"Urban","year":"2005"},{"key":"S0956796813000245_ref54","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"S0956796813000245_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45699-6_8"},{"key":"S0956796813000245_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/359138.359142"},{"key":"S0956796813000245_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796813000245_ref23","first-page":"45","volume-title":"Proceedings of the 23rd International Conference on Logic Programming (ICLP 2007)","author":"Hanus","year":"2007"},{"key":"S0956796813000245_ref25","first-page":"202","volume-title":"Proceedings of the 2nd International ACM-SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2000)","author":"Hanus","year":"2000"},{"key":"S0956796813000245_ref32","first-page":"47","volume-title":"Proceedings of the 18th European Symposium on Programming (ESOP 2009)","author":"Lakin","year":"2009"},{"key":"S0956796813000245_ref38","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"S0956796813000245_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_16"},{"key":"S0956796813000245_ref30","unstructured":"Lakin M. R. (2010) An Executable Meta-language for Inductive Definitions with Binders, PhD thesis, University of Cambridge, UK."},{"key":"S0956796813000245_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"S0956796813000245_ref65","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"},{"key":"S0956796813000245_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"S0956796813000245_ref7","first-page":"265","volume-title":"Proceedings of the 21st International Conference on Logic Programming (ICLP 2005)","author":"Bra\u00dfel","year":"2005"},{"key":"S0956796813000245_ref58","first-page":"1","volume-title":"Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP 2007)","author":"Sewell","year":"2007"},{"key":"S0956796813000245_ref51","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.006"},{"key":"S0956796813000245_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"S0956796813000245_ref1","first-page":"1","volume-title":"Proceedings of the 11th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2002)","author":"Albert","year":"2002"},{"key":"S0956796813000245_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9164-3"},{"key":"S0956796813000245_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0056-1"},{"key":"S0956796813000245_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10002-X"},{"key":"S0956796813000245_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"S0956796813000245_ref42","first-page":"810","volume-title":"Proceedings of the 5th International Conference on Logic Programming (ICLP 1988)","author":"Nadathur","year":"1988"},{"key":"S0956796813000245_ref52","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(1:4)2008"},{"key":"S0956796813000245_ref61","first-page":"263","volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003)","author":"Shinwell","year":"2003"},{"key":"S0956796813000245_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"S0956796813000245_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796813000245","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:05Z","timestamp":1779834965000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796813000245\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":66,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["S0956796813000245"],"URL":"https:\/\/doi.org\/10.1017\/s0956796813000245","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]}}}