{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:16Z","timestamp":1779836716487,"version":"3.53.1"},"reference-count":15,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5608,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1993,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    A binding-time analysis is correct if it always produces\n                    <jats:italic>consistent<\/jats:italic>\n                    binding-time information. Consistency prevents partial evaluators from \u2018going wrong\u2019. A sufficient and decidable condition for consistency, called well-annotatedness, was first presented by Gomard and Jones. In this paper we prove that a weaker condition implies consistency. Our condition is decidable, subsumes the one of Gomard and Jones, and was first studied by Schwartzbach and the present author. Our result implies the correctness of the binding-time analysis of Mogensen, and it indicates the correctness of the core of the binding-time analyses of Bondorf and Consel. We also prove that\n                    <jats:italic>all<\/jats:italic>\n                    partial evaluators will on termination have eliminated all \u2018eliminable\u2019-marked parts of an input which satisfies our condition. This generalizes a result of Gomard. Our development is for the pure \u03bb-calculus with explicit binding-time annotations.\n                  <\/jats:p>","DOI":"10.1017\/s0956796800000770","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:13:56Z","timestamp":1226056436000},"page":"347-363","source":"Crossref","is-referenced-by-count":26,"title":["Correctness of binding-time analysis"],"prefix":"10.1017","volume":"3","author":[{"given":"Jens","family":"Palsberg","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000770_ref006","unstructured":"Gomard Carsten K. (1991) (November). Program analysis matters. Ph.D. thesis, DIKU, University of Copenhagen. DIKU Report 91\u201317."},{"key":"S0956796800000770_ref015","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000782"},{"key":"S0956796800000770_ref009","unstructured":"Mogensen Torben \u00c6 . (1992) Self-applicable partial evaluation for pure lambda calculus. Pages 116\u2013121 of: Proc. ACM SIGPLAN workshop on partial evaluation and semantics-based program manipulation."},{"key":"S0956796800000770_ref013","doi-asserted-by":"crossref","unstructured":"Sestoft Peter . (1989) Replacing function parameters by global variables. Pages 39\u201353 of: Proc. conference on functional programming languages and computer architecture.","DOI":"10.1145\/99370.99374"},{"key":"S0956796800000770_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10843-2_10"},{"key":"S0956796800000770_ref004","doi-asserted-by":"crossref","unstructured":"Consel Charles . (1990) Binding-time analysis for higher order untyped functional languages. Pages 264\u2013272 of: Proc. ACM conference on lisp and functional programming.","DOI":"10.1145\/91556.91668"},{"key":"S0956796800000770_ref011","doi-asserted-by":"crossref","unstructured":"Palsberg Jens , & Schwartzbach Michael I. (1992) Binding-time analysis: Abstract interpretation versus type inference. Submitted for publication.","DOI":"10.7146\/dpb.v21i393.6628"},{"key":"S0956796800000770_ref003","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000769"},{"key":"S0956796800000770_ref005","doi-asserted-by":"crossref","unstructured":"Gomard Carsten K. (1990) Partial type inference for untyped functional programs. Pages 282\u2013287 of: Proc. ACM conference on lisp and functional programming.","DOI":"10.1145\/91556.91672"},{"key":"S0956796800000770_ref001","volume-title":"The lambda calculus: Its syntax and semantics","author":"Barendregt","year":"1981"},{"key":"S0956796800000770_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90035-V"},{"key":"S0956796800000770_ref007","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000058"},{"key":"S0956796800000770_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90025-1"},{"key":"S0956796800000770_ref012","first-page":"295","volume-title":"Proc. partial evaluation and mixed computation","author":"Schmidt","year":"1987"},{"key":"S0956796800000770_ref014","unstructured":"Shivers Olin . (1991) (May). Control-flow analysis of higher-order languages. Ph.D. thesis, CMU. CMU-CS-91-145."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000770","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:11Z","timestamp":1779834911000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000770\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,7]]},"references-count":15,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,7]]}},"alternative-id":["S0956796800000770"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000770","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,7]]}}}