{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:54:01Z","timestamp":1776891241054,"version":"3.51.2"},"reference-count":38,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"4","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4786,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1995,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper presents semantic specifications and correctness proofs for both on-line and offline partial evaluation of strict first-order functional programs. To do so, our strategy consists of defining a\n                    <jats:italic>core semantics<\/jats:italic>\n                    as a basis for the specification of three non-standard evaluations: instrumented evaluation, on-line and off-line partial evaluation. We then use the technique of\n                    <jats:italic>logical relations<\/jats:italic>\n                    to prove the correctness of both on-line and off-line partial evaluation semantics.\n                  <\/jats:p>\n                  <jats:p>The contributions of this work are as follows:<\/jats:p>\n                  <jats:p>\n                    1. We provide a\n                    <jats:italic>uniform framework<\/jats:italic>\n                    to defining and proving correct both on-line and off-line partial evaluation.\n                  <\/jats:p>\n                  <jats:p>2. This work required a formal specification of on-line partial evaluation with polyvariant specialization. We define criteria for its correctness with respect to an instrumented standard semantics. As a by-product, on-line partial evaluation appears to be based on a fixpoint iteration process, just like binding-time analysis.<\/jats:p>\n                  <jats:p>\n                    3. We show that binding-time analysis, the preprocessing phase of off-line partial evaluation, is an\n                    <jats:italic>abstraction<\/jats:italic>\n                    of on-line partial evaluation. Therefore, its correctness can be proved with respect to on-line partial evaluation, instead of with respect to the standard semantics, as is customarily done.\n                  <\/jats:p>\n                  <jats:p>\n                    4. Based on the binding-time analysis, we formally\n                    <jats:italic>derive<\/jats:italic>\n                    the specialization semantics for off-line partial evaluation. This strategy ensures the correctness of the resulting semantics.\n                  <\/jats:p>","DOI":"10.1017\/s0956796800001453","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:11:23Z","timestamp":1226056283000},"page":"461-500","source":"Crossref","is-referenced-by-count":5,"title":["On-line and off-line partial evaluation: semantic specifications and correctness proofs"],"prefix":"10.46298","volume":"5","author":[{"given":"Charles","family":"Consel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siau Cheng","family":"Khoo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001453_ref037","doi-asserted-by":"crossref","unstructured":"Wand M. (1993) Specifying the correctness of binding-time analysis. In: ACM Symposium on Principles of Programming Languages, pp. 137\u2013143.","DOI":"10.1145\/158511.158614"},{"key":"S0956796800001453_ref034","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526572"},{"key":"S0956796800001453_ref032","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90025-1"},{"key":"S0956796800001453_ref031","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90091-1"},{"key":"S0956796800001453_ref015","doi-asserted-by":"crossref","unstructured":"Hannan J. and Miller D. (1989) Deriving Mixed Evaluation From Standard Evaluation For a Simple Functional Language. Technical Report MS-CIS-89-28, University of Pennsylvania, Philadelphia, PA.","DOI":"10.1007\/3-540-51305-1_13"},{"key":"S0956796800001453_ref028","doi-asserted-by":"crossref","unstructured":"Launchbury J. (1990) Projection Factorisation in Partial Evaluation. PhD thesis, Department of Computing Science, University of Glasgow, Scotland.","DOI":"10.1017\/CBO9780511569814"},{"key":"S0956796800001453_ref036","volume-title":"Partial Evaluation and Mixed Computation","author":"Sestoft","year":"1988"},{"key":"S0956796800001453_ref004","unstructured":"Colby C. and Lee P. (1991) An implementation of parameterized partial evaluation. In: Workshop on Static Analysis, pp. 82\u201389, Bigre Journal."},{"key":"S0956796800001453_ref029","first-page":"116","volume-title":"ACM Workshop on Partial Evaluation and Semantics-Based Program Manipulation","author":"Mogensen","year":"1992"},{"key":"S0956796800001453_ref008","doi-asserted-by":"crossref","unstructured":"Consel C. and Danvy D. (1990) From interpreting to compiling binding times. In: Jones N. D. (ed.), ESOP'90: 3rd European Symposium on Programming, pp. 88\u2013105. Springer-Verlag.","DOI":"10.1007\/3-540-52592-0_57"},{"key":"S0956796800001453_ref024","volume-title":"Abstract Interpretation: a Semantics-Based Tool for Program Analysis","author":"Jones","year":"1990"},{"key":"S0956796800001453_ref007","doi-asserted-by":"crossref","unstructured":"Consel C. (1993b) A tour of Schism: a partial evaluation system for higher-order applicative languages. In: ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 66\u201377.","DOI":"10.1145\/154630.154645"},{"key":"S0956796800001453_ref010","doi-asserted-by":"crossref","unstructured":"Consel C. and Khoo S. C. (1991) Parameterized partial evaluation. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 92\u2013106.","DOI":"10.1145\/113445.113454"},{"key":"S0956796800001453_ref021","unstructured":"Jones N. D. (1991) A minimal function graph semantics as a basis for abstract interpretation of higher order programs. Presented at the 1991 Workshop on Static Analysis of Equational, Functional and Logic Programs."},{"key":"S0956796800001453_ref026","unstructured":"Kleene S. C. . Introduction to Metamathematics. Van Nostrand, 1952."},{"key":"S0956796800001453_ref006","doi-asserted-by":"crossref","unstructured":"Consel C. (1993a) Polyvariant binding-time analysis for higher-order, applicative languages. In: ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pap. 145\u2013154.","DOI":"10.1145\/154630.154638"},{"key":"S0956796800001453_ref005","doi-asserted-by":"crossref","unstructured":"Consel C. (1988) New insights into partial evaluation: the Schism experiment. In: Ganzinger H. (ed.), ESOP'88: 2nd European Symposium on Programming, pp. 236\u2013246. Springer-Verlag.","DOI":"10.1007\/3-540-19027-9_16"},{"key":"S0956796800001453_ref023","doi-asserted-by":"crossref","unstructured":"Jones N. D. and Mycroft A. (1986) Data flow analysis of applicative programs using minimal function graphs. In: ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/512644.512672"},{"key":"S0956796800001453_ref009","doi-asserted-by":"crossref","unstructured":"Consel C. and Danvy D. (1993) Tutorial notes on partial evaluation. In: ACM Symposium on Principles of Programming Languages, pp. 493\u2013501.","DOI":"10.1145\/158511.158707"},{"key":"S0956796800001453_ref001","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.1.5"},{"key":"S0956796800001453_ref027","unstructured":"Khoo S. C. (1992) Parameterized Partial Evaluation: Theory and Practice. PhD thesis, Yale University. (Research Report 926.)"},{"key":"S0956796800001453_ref003","volume-title":"Binding Time Analysis and the Taming of Self-Application","author":"Bondorf","year":"1988"},{"key":"S0956796800001453_ref018","first-page":"225","volume-title":"Partial Evaluation and Mixed Computation","author":"Jones","year":"1988"},{"key":"S0956796800001453_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90035-V"},{"key":"S0956796800001453_ref012","first-page":"45","article-title":"Partial evaluation of computation process \u2013 an approach to a compiler-compiler","volume":"2","author":"Futamura","year":"1971","journal-title":"Systems, Computers, Controls"},{"key":"S0956796800001453_ref038","volume-title":"Computing Types During Program Specialization","author":"Weise","year":"1990"},{"key":"S0956796800001453_ref033","doi-asserted-by":"crossref","unstructured":"Nielson H. R. and Nielson F. (1988b) Automatic binding time analysis for a typed \u03bb-calculus. In: ACM Symposium on Principles of Programming Languages, pp. 98\u2013106.","DOI":"10.1145\/73560.73569"},{"key":"S0956796800001453_ref011","doi-asserted-by":"publisher","DOI":"10.1145\/169683.174155"},{"key":"S0956796800001453_ref022","unstructured":"Jones N. D. and Muchnick S. S. (1976) Some thoughts towards the design of an ideal language. In: ACM Conference on Principles of Programming Languages, pp. 77\u201394."},{"key":"S0956796800001453_ref013","volume-title":"Programs as Data Objects. Lecture Notes in Computer Science 217","author":"Ganzinger","year":"1985"},{"key":"S0956796800001453_ref016","unstructured":"Holst C. K. (1989) Program Specialization for Compiler Generation. Master's thesis, University of Copenhagen, DIKU, Denmark."},{"key":"S0956796800001453_ref017","doi-asserted-by":"crossref","unstructured":"Hudak P. and Young J. (1988) A collecting interpretation of expressions (without Powerdomains). In: ACM Symposium on Principles of Programming Languages, pp. 107\u2013118.","DOI":"10.1145\/73560.73570"},{"key":"S0956796800001453_ref035","first-page":"236","volume-title":"Programs as Data Objects. Lecture Notes in Computer Science 217","author":"Sestoft","year":"1985"},{"key":"S0956796800001453_ref020","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032064"},{"key":"S0956796800001453_ref019","volume-title":"Binding Time Analysis and Static Semantics (extended abstract)","author":"Jones","year":"1988"},{"key":"S0956796800001453_ref014","doi-asserted-by":"publisher","DOI":"10.1145\/128861.128864"},{"key":"S0956796800001453_ref030","volume-title":"A Security Flow Control Algorithm and Its Denotational Semantics Correctness Proof","author":"Mizuno","year":"1990"},{"key":"S0956796800001453_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF01806312"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001453","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:18:06Z","timestamp":1776889086000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001453\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,10]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,10]]}},"alternative-id":["S0956796800001453"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001453","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,10]]}}}