{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:30Z","timestamp":1775790750905,"version":"3.50.1"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2004,7,1]],"date-time":"2004-07-01T00:00:00Z","timestamp":1088640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2004,7]]},"abstract":"<jats:p>We present a framework for offline partial evaluation for call-by-value functional programming languages with an ML-style typing discipline. This includes a binding-time analysis which is (1) polymorphic with respect to binding times; (2) allows the use of polymorphic recursion with respect to binding times; (3) is applicable to a polymorphically typed term; and (4) is proven correct with respect to a novel small-step specialization semantics.The main innovation is to build the analysis on top of the region calculus of Tofte and Talpin [1994], thus leveraging the tools and techniques developed for it. Our approach factorizes the binding-time analysis into region inference and a subsequent constraint analysis. The key insight underlying our framework is to consider binding times as properties of regions.Specialization is specified as a small-step semantics, building on previous work on syntactic-type soundness results for the region calculus. Using similar syntactic proof techniques, we prove soundness of the binding-time analysis with respect to the specializer. In addition, we prove that specialization preserves the call-by-value semantics of the region calculus by showing that the reductions of the specializer are contextual equivalences in the region calculus.<\/jats:p>","DOI":"10.1145\/1011508.1011510","type":"journal-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T17:38:56Z","timestamp":1097170736000},"page":"652-701","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Polymorphic specialization for ML"],"prefix":"10.1145","volume":"26","author":[{"given":"Simon","family":"Helsen","sequence":"first","affiliation":[{"name":"University of Waterloo, Canada"}]},{"given":"Peter","family":"Thiemann","sequence":"additional","affiliation":[{"name":"Universit\u00e4t Freiburg, Germany"}]}],"member":"320","published-online":{"date-parts":[[2004,7]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 1999 ACM SIGPLAN Symposium on Principles of Programming Languages (San Antonio, Tex). ACM","author":"Abadi M.","unstructured":"Abadi , M. , Banerjee , A. , Heintze , N. , and Riecke , J . 1999. A core calculus of dependency . In Proceedings of the 1999 ACM SIGPLAN Symposium on Principles of Programming Languages (San Antonio, Tex). ACM , New York, 147--160.]] 10.1145\/292540.292555 Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. 1999. A core calculus of dependency. In Proceedings of the 1999 ACM SIGPLAN Symposium on Principles of Programming Languages (San Antonio, Tex). ACM, New York, 147--160.]] 10.1145\/292540.292555"},{"key":"e_1_2_1_2_1","volume-title":"proceedings of the 14th Annual Symposium on Logic in Computer Science, LICS'99","author":"Banerjee A.","unstructured":"Banerjee , A. , Heintze , N. , and Riecke , J . 1999. Region analysis and the polymorphic lambda calculus . In proceedings of the 14th Annual Symposium on Logic in Computer Science, LICS'99 ( Trento, Italy). IEEE Computer Society Press, Los Alamitos, Calif., 88--97.]] Banerjee, A., Heintze, N., and Riecke, J. 1999. Region analysis and the polymorphic lambda calculus. In proceedings of the 14th Annual Symposium on Logic in Computer Science, LICS'99 (Trento, Italy). IEEE Computer Society Press, Los Alamitos, Calif., 88--97.]]"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00025-6"},{"key":"e_1_2_1_4_1","unstructured":"Birkedal L. and Welinder M. 1993. Partial evaluation of Standard ML. Rapport 93\/22 DIKU University of Copenhagen.]] Birkedal L. and Welinder M. 1993. Partial evaluation of Standard ML. Rapport 93\/22 DIKU University of Copenhagen.]]"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 1994 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (Orlando, Fla), 61--71","author":"Birkedal L.","unstructured":"Birkedal , L. and Welinder , M . 1994. Binding-time analysis for Standard-ML . In Proceedings of the 1994 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (Orlando, Fla), 61--71 . (Technical Report 94\/9, Department of Computer Science.)]] Birkedal, L. and Welinder, M. 1994. Binding-time analysis for Standard-ML. In Proceedings of the 1994 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (Orlando, Fla), 61--71. (Technical Report 94\/9, Department of Computer Science.)]]"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0956796800000769","article-title":"Efficient analyses for realistic off-line partial evaluation","volume":"3","author":"Bondorf A.","year":"1993","unstructured":"Bondorf , A. and J\u00f8rgensen , J. 1993 . Efficient analyses for realistic off-line partial evaluation . J. Funct. Prog. 3 , 3 (July), 315--346.]] Bondorf, A. and J\u00f8rgensen, J. 1993. Efficient analyses for realistic off-line partial evaluation. J. Funct. Prog. 3, 3 (July), 315--346.]]","journal-title":"J. Funct. Prog."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation","author":"Bulyonkov M.","year":"1993","unstructured":"Bulyonkov , M. 1993 . Extracting polyvariant binding time analysis from polyvariant specializer . In Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation ( Copenhagen, Denmark), D. Schmidt, Ed. ACM, New York, 59--65.]] 10.1145\/154630.154637 Bulyonkov, M. 1993. Extracting polyvariant binding time analysis from polyvariant specializer. In Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (Copenhagen, Denmark), D. Schmidt, Ed. ACM, New York, 59--65.]] 10.1145\/154630.154637"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 2001 ASM SIGPLAN Symposium on Principles of Programming Languages","author":"Calcagno C.","year":"2001","unstructured":"Calcagno , C. 2001 . Stratified operational semantics for safety and correctness of the region calculus . In Proceedings of the 2001 ASM SIGPLAN Symposium on Principles of Programming Languages ( London, England), H. R. Nielson, Ed. ACM, New York, 155--165.]] 10.1145\/360204.360217 Calcagno, C. 2001. Stratified operational semantics for safety and correctness of the region calculus. In Proceedings of the 2001 ASM SIGPLAN Symposium on Principles of Programming Languages (London, England), H. R. Nielson, Ed. ACM, New York, 155--165.]] 10.1145\/360204.360217"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3112"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 1990 ACM Conference on Lisp and Functional Programming","author":"Consel C.","year":"1990","unstructured":"Consel , C. 1990 . Binding time analysis for higher order untyped functional languages . In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming ( Nice, France). ACM, New York, 264--272.]] 10.1145\/91556.91668 Consel, C. 1990. Binding time analysis for higher order untyped functional languages. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming (Nice, France). ACM, New York, 264--272.]] 10.1145\/91556.91668"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evalution and Semantics-Based Program Manipulation","author":"Consel C.","year":"1993","unstructured":"Consel , C. 1993 a. Polyvariant binding-time analysis for applicative languages . In Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evalution and Semantics-Based Program Manipulation ( Copenhagen, Denmark), D. Schmidt, Ed. ACM, New York, 66--77.]] 10.1145\/154630.154638 Consel, C. 1993a. Polyvariant binding-time analysis for applicative languages. In Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evalution and Semantics-Based Program Manipulation (Copenhagen, Denmark), D. Schmidt, Ed. ACM, New York, 66--77.]] 10.1145\/154630.154638"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evalution and Semantics-Based Program Manipulation","author":"Consel C.","year":"1993","unstructured":"Consel , C. 1993 b. A tour of Schism . In Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evalution and Semantics-Based Program Manipulation ( Copenhagen, Denmark), D. Schmidt, Ed. ACM, New York, 134--154.]] 10.1145\/154630.154645 Consel, C. 1993b. A tour of Schism. In Proceedings of the 1993 ACM SIGPLAN Workshop on Partial Evalution and Semantics-Based Program Manipulation (Copenhagen, Denmark), D. Schmidt, Ed. ACM, New York, 134--154.]] 10.1145\/154630.154645"},{"key":"e_1_2_1_14_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"523","author":"Consel C.","unstructured":"Consel , C. and Danvy , O . 1991. For a better support of static data flow. In Functional Prgramming Languages and Computer Architecture (Cambridge, Mass.), J. Hughes , Ed. Lecture Notes in Computer Science , vol. 523 . Springer-Verlag, New York, 496--519.]] Consel, C. and Danvy, O. 1991. For a better support of static data flow. In Functional Prgramming Languages and Computer Architecture (Cambridge, Mass.), J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523. Springer-Verlag, New York, 496--519.]]"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 1993 ACM SIGPLAN Symposium on Principles of Programming Languages (Charleston, S.C.). ACM","author":"Consel C.","unstructured":"Consel , C. and Danvy , O . 1993. Tutorial notes on partial evaluation . In Proceedings of the 1993 ACM SIGPLAN Symposium on Principles of Programming Languages (Charleston, S.C.). ACM , New York, 493--501.]] 10.1145\/158511.158707 Consel, C. and Danvy, O. 1993. Tutorial notes on partial evaluation. In Proceedings of the 1993 ACM SIGPLAN Symposium on Principles of Programming Languages (Charleston, S.C.). ACM, New York, 493--501.]] 10.1145\/158511.158707"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019004"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/236114.236119"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 1997 Conference on Programming Language Design and Implementation (Las Vegas, Nev.). ACM","author":"Dussart D.","unstructured":"Dussart , D. , Heldal , R. , and Hughes , J . 1997. Module-sensitive program specialisation . In Proceedings of the 1997 Conference on Programming Language Design and Implementation (Las Vegas, Nev.). ACM , New York, 206--214.]] 10.1145\/258915.258934 Dussart, D., Heldal, R., and Hughes, J. 1997. Module-sensitive program specialisation. In Proceedings of the 1997 Conference on Programming Language Design and Implementation (Las Vegas, Nev.). ACM, New York, 206--214.]] 10.1145\/258915.258934"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 1995 International Static Analysis Symposium (Glasgow, Scotland), A. Mycroft, Ed. Lecture Notes in Computer Science","volume":"983","author":"Dussart D.","unstructured":"Dussart , D. , Henglein , F. , and Mossin , C . 1995. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time . In Proceedings of the 1995 International Static Analysis Symposium (Glasgow, Scotland), A. Mycroft, Ed. Lecture Notes in Computer Science , vol. 983 , Springer-Verlag, New York, 118--136.]] Dussart, D., Henglein, F., and Mossin, C. 1995. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Proceedings of the 1995 International Static Analysis Symposium (Glasgow, Scotland), A. Mycroft, Ed. Lecture Notes in Computer Science, vol. 983, Springer-Verlag, New York, 118--136.]]"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 2nd Workshop on Static Analysis. Bigre Journal","volume":"82","author":"Gengler M.","unstructured":"Gengler , M. , and Rytz , B . 1992. A polyvariant binding time analysis handling partially known values . In Proceedings of the 2nd Workshop on Static Analysis. Bigre Journal , vol. 81-- 82 . IRISA, Rennes, France, 322--330.]] Gengler, M., and Rytz, B. 1992. A polyvariant binding time analysis handling partially known values. In Proceedings of the 2nd Workshop on Static Analysis. Bigre Journal, vol. 81--82. IRISA, Rennes, France, 322--330.]]"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 1986 ACM Conference on LISP and Functional Programming. ACM","author":"Gifford D.","year":"1983","unstructured":"Gifford , D. and Lucassen , J . 1986. Integrating functional and imperative programming . In Proceedings of the 1986 ACM Conference on LISP and Functional Programming. ACM , New York, 28--38.]] 10.1145\/3 1983 8.319848 Gifford, D. and Lucassen, J. 1986. Integrating functional and imperative programming. In Proceedings of the 1986 ACM Conference on LISP and Functional Programming. ACM, New York, 28--38.]] 10.1145\/319838.319848"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Glenstrup A. J. and Jones N. D . 1996 . BTA algorithms to ensure termination of offline partial evaluation. In PSA-96: Andrei Ershov Second International Memorial Conference Perspectives of System Informatics (Novosibirsk Russia) Lecture Notes in Computer Science vol. 1181 . Springer-Verlag New York 273--284.]] Glenstrup A. J. and Jones N. D. 1996. BTA algorithms to ensure termination of offline partial evaluation. In PSA-96: Andrei Ershov Second International Memorial Conference Perspectives of System Informatics (Novosibirsk Russia) Lecture Notes in Computer Science vol. 1181. Springer-Verlag New York 273--284.]]","DOI":"10.1007\/3-540-62064-8_23"},{"key":"e_1_2_1_24_1","volume-title":"Lecture Notes in Computer Science","volume":"2053","author":"Glynn K.","unstructured":"Glynn , K. , Stuckey , P. , Sulzmann , M. , and S\u00f8ndergaard , H . 2001. Boolean constraints for binding-time analysis. In Programs as Data Objects II (Aarhus, Denmark) . Lecture Notes in Computer Science , vol. 2053 . Springer-Verlag, New York, 39--62.]] Glynn, K., Stuckey, P., Sulzmann, M., and S\u00f8ndergaard, H. 2001. Boolean constraints for binding-time analysis. In Programs as Data Objects II (Aarhus, Denmark). Lecture Notes in Computer Science, vol. 2053. Springer-Verlag, New York, 39--62.]]"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00178-6"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002405"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00050-5"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Heldal R. and Hughes J . 2001 . Binding-time analysis for polymorphic types. In PSI-01: Andrei Ershov Fourth International Conference Perspectives of System Informatics (Novosibirsk Russia) Lecture Notes in Computer Science vol. 2244 . Springer-Verlag New York 191--204.]] Heldal R. and Hughes J. 2001. Binding-time analysis for polymorphic types. In PSI-01: Andrei Ershov Fourth International Conference Perspectives of System Informatics (Novosibirsk Russia) Lecture Notes in Computer Science vol. 2244. Springer-Verlag New York 191--204.]]","DOI":"10.1007\/3-540-45575-2_19"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-004-4868-x"},{"key":"e_1_2_1_33_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"1927","author":"Helsen S.","unstructured":"Helsen , S. and Thiemann , P . 2000a. Fragmental specialization. In Semantics, Applications and Implementation of Program Generation (SAIG'00) (Montreal, Ont., Canada), W. Taha , Ed. Lecture Notes in Computer Science , vol. 1927 . Springer-Verlag, New York, 51--71.]] Helsen, S. and Thiemann, P. 2000a. Fragmental specialization. In Semantics, Applications and Implementation of Program Generation (SAIG'00) (Montreal, Ont., Canada), W. Taha, Ed. Lecture Notes in Computer Science, vol. 1927. Springer-Verlag, New York, 51--71.]]"},{"key":"e_1_2_1_34_1","volume-title":"ACM Workshop on Higher Order Operational Techniques in Semantics (HOOTS) (Montreal, Ont., Canada). A. Jeffrey, Ed. Electronic Notes in Theoretical Computer Science","volume":"20","author":"Helsen S.","unstructured":"Helsen , S. and Thiemann , P . 2000b. Syntactic type soundness for the region calculus . In ACM Workshop on Higher Order Operational Techniques in Semantics (HOOTS) (Montreal, Ont., Canada). A. Jeffrey, Ed. Electronic Notes in Theoretical Computer Science , vol. 41(3). Elsevier Science, Amsterdam, The Netherlands 1-- 20 .]] Helsen, S. and Thiemann, P. 2000b. Syntactic type soundness for the region calculus. In ACM Workshop on Higher Order Operational Techniques in Semantics (HOOTS) (Montreal, Ont., Canada). A. Jeffrey, Ed. Electronic Notes in Theoretical Computer Science, vol. 41(3). Elsevier Science, Amsterdam, The Netherlands 1--20.]]"},{"key":"e_1_2_1_35_1","volume-title":"Efficient type interference for higher-order binding-time analysis","author":"Henglein F.","unstructured":"Henglein , F. 1991. Efficient type interference for higher-order binding-time analysis . In Functional Programming Languages and Computer Architecture (Cambridge, Mass .), J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523 . Springer-Verlag , New York, 448--472.]] Henglein, F. 1991. Efficient type interference for higher-order binding-time analysis. In Functional Programming Languages and Computer Architecture (Cambridge, Mass.), J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523. Springer-Verlag, New York, 448--472.]]"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of European Symposium on Programming, D. Sannella, Ed. Lecture Notes in Computer Science","volume":"788","author":"Henglein F.","unstructured":"Henglein , F. , and Mossin , C . 1994. Polymorphic binding-time analysis . In Proceedings of European Symposium on Programming, D. Sannella, Ed. Lecture Notes in Computer Science , vol. 788 . Springer-Verlag, New York 287--301.]] Henglein, F., and Mossin, C. 1994. Polymorphic binding-time analysis. In Proceedings of European Symposium on Programming, D. Sannella, Ed. Lecture Notes in Computer Science, vol. 788. Springer-Verlag, New York 287--301.]]"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00048-7"},{"key":"e_1_2_1_38_1","unstructured":"Jones N. Gomard C. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall Englewood Cliffs N.J.]] Jones N. Gomard C. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall Englewood Cliffs N.J.]]"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 1991 ACM SIGPLAN Symposium on Principles of Programming Languages","author":"Jouvelot P.","unstructured":"Jouvelot , P. and Gifford , D . 1991. Algebraic reconstruction of types and effects . In Proceedings of the 1991 ACM SIGPLAN Symposium on Principles of Programming Languages ( Orlando, Florida), ACM New York, 303--310.]] 10.1145\/99583.99623 Jouvelot, P. and Gifford, D. 1991. Algebraic reconstruction of types and effects. In Proceedings of the 1991 ACM SIGPLAN Symposium on Principles of Programming Languages (Orlando, Florida), ACM New York, 303--310.]] 10.1145\/99583.99623"},{"key":"e_1_2_1_40_1","volume-title":"Higher Order Operational Techniques in Semantics (HOOTS)","author":"Lassen S.","unstructured":"Lassen , S. 1998. Relational reasoning about contexts . In Higher Order Operational Techniques in Semantics (HOOTS) , A. Gordon and A. Pitts, Eds. Publications of the Newton Institute. Cambridge University Press , 91--136.]] Lassen, S. 1998. Relational reasoning about contexts. In Higher Order Operational Techniques in Semantics (HOOTS), A. Gordon and A. Pitts, Eds. Publications of the Newton Institute. Cambridge University Press, 91--136.]]"},{"key":"e_1_2_1_41_1","volume-title":"Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming","author":"Launchbury J.","unstructured":"Launchbury , J. and Holst , C. K . 1991. Handwriting cogen to avoid problems with static typing . In Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming . Glasgow University, Skye, Scotland, 210--218.]] Launchbury, J. and Holst, C. K. 1991. Handwriting cogen to avoid problems with static typing. In Draft Proceedings, Fourth Annual Glasgow Workshop on Functional Programming. Glasgow University, Skye, Scotland, 210--218.]]"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Lawall J. and Thiemann P . 1997 . Sound specialization in the presence of computational effects. In Proceedings of the Theoretical Aspects of Computer Software (Sendai Japan) Lecture Notes in Computer Science vol. 1284 Springer-Verlag New York 165--190.]] Lawall J. and Thiemann P. 1997. Sound specialization in the presence of computational effects. In Proceedings of the Theoretical Aspects of Computer Software (Sendai Japan) Lecture Notes in Computer Science vol. 1284 Springer-Verlag New York 165--190.]]","DOI":"10.1007\/BFb0014551"},{"key":"e_1_2_1_43_1","volume-title":"Static Analysis: 9th International Symposium, SAS","volume":"2477","author":"Lee C. S.","year":"2002","unstructured":"Lee , C. S. 2002 a. Finiteness analysis in polynomial time . In Static Analysis: 9th International Symposium, SAS 2002, M. Hermenegildo and G. Puebla, Eds. Lecture Notes in Computer Science , vol. 2477 . Springer-Verlag, New York, 493--508.]] Lee, C. S. 2002a. Finiteness analysis in polynomial time. In Static Analysis: 9th International Symposium, SAS 2002, M. Hermenegildo and G. Puebla, Eds. Lecture Notes in Computer Science, vol. 2477. Springer-Verlag, New York, 493--508.]]"},{"key":"e_1_2_1_44_1","volume-title":"Generative Programming and Component Engineering: ACM SIGPLAN\/SIGSOFT Conference, GPCE","volume":"2487","author":"Lee C. S.","year":"2002","unstructured":"Lee , C. S. 2002 b. Program termination analysis in polynomial time . In Generative Programming and Component Engineering: ACM SIGPLAN\/SIGSOFT Conference, GPCE 2002, D. Batory, C. Consel, and W. Taha, Eds. Lecture Notes in Computer Science , vol. 2487 . Springer-Verlag, New York, 218--235.]] Lee, C. S. 2002b. Program termination analysis in polynomial time. In Generative Programming and Component Engineering: ACM SIGPLAN\/SIGSOFT Conference, GPCE 2002, D. Batory, C. Consel, and W. Taha, Eds. Lecture Notes in Computer Science, vol. 2487. Springer-Verlag, New York, 218--235.]]"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 2001 ACM SIGPLAN Symposium on Principles of Programming Languages","author":"Lee C. S.","unstructured":"Lee , C. S. , Jones , N. D. , and Ben-Amram , A. M . 2001. The size-change principle for program termination . In Proceedings of the 2001 ACM SIGPLAN Symposium on Principles of Programming Languages ( London, England), H. R. Nielson, Ed. ACM New York, 81--92.]] 10.1145\/360204.360210 Lee, C. S., Jones, N. D., and Ben-Amram, A. M. 2001. The size-change principle for program termination. In Proceedings of the 2001 ACM SIGPLAN Symposium on Principles of Programming Languages (London, England), H. R. Nielson, Ed. ACM New York, 81--92.]] 10.1145\/360204.360210"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","article-title":"A theory of type polymorphism in programming","volume":"17","author":"Milner R.","year":"1978","unstructured":"Milner , R. 1978 . A theory of type polymorphism in programming . J. Comput. Syst. Sci. 17 , 348 -- 375 .]] Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Milner R. Tofte M. Harper R. and MacQueen D. 1997. The Definition of Standard ML (Revised). MIT Press Cambridge Mass.]] Milner R. Tofte M. Harper R. and MacQueen D. 1997. The Definition of Standard ML (Revised). MIT Press Cambridge Mass.]]","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"e_1_2_1_48_1","volume-title":"TAPSOFT '89","volume":"351","author":"Mogensen T.","year":"1989","unstructured":"Mogensen , T. 1989 . Binding time analysis for polymorphically typed higher order languages . In TAPSOFT '89 ( Barcelona, Spain), J. D\u00edaz and F. Orejas, Eds. Lecture Notes in Computer Science , vol. 351 and 352. Springer-Verlag, New York, 298--312.]] Mogensen, T. 1989. Binding time analysis for polymorphically typed higher order languages. In TAPSOFT '89 (Barcelona, Spain), J. D\u00edaz and F. Orejas, Eds. Lecture Notes in Computer Science, vol. 351 and 352. Springer-Verlag, New York, 298--312.]]"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(88)90025-1"},{"key":"e_1_2_1_52_1","volume-title":"Two-Level Functional Languages. Cambridge Tracts in Theoretical Computer Science","volume":"34","author":"Nielson F.","unstructured":"Nielson , F. and Nielson , H. R . 1992 . Two-Level Functional Languages. Cambridge Tracts in Theoretical Computer Science , vol. 34 . Cambridge University Press, Cambridge, Mass.]] Nielson, F. and Nielson, H. R. 1992. Two-Level Functional Languages. Cambridge Tracts in Theoretical Computer Science, vol. 34. Cambridge University Press, Cambridge, Mass.]]"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1%3C35::AID-TAPO4%3E3.0.CO;2-4"},{"key":"e_1_2_1_54_1","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","article-title":"Call-by-name, call-by-value and the \u03bb-calculus","volume":"1","author":"Plotkin G.","year":"1975","unstructured":"Plotkin , G. 1975 . Call-by-name, call-by-value and the \u03bb-calculus . Theoret. Comput. Sci. 1 , 125 -- 159 .]] Plotkin, G. 1975. Call-by-name, call-by-value and the \u03bb-calculus. Theoret. Comput. Sci. 1, 125--159.]]","journal-title":"Theoret. Comput. Sci."},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the 1992 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, C. Consel, Ed","author":"Rytz B.","unstructured":"Rytz , B. and Gengler , M . 1992. A polyvariant binding time analysis . In Proceedings of the 1992 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, C. Consel, Ed . Yale University, San Francisco, CA, 21--28. Report YALEU\/DCS\/RR-909.]] Rytz, B. and Gengler, M. 1992. A polyvariant binding time analysis. In Proceedings of the 1992 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, C. Consel, Ed. Yale University, San Francisco, CA, 21--28. Report YALEU\/DCS\/RR-909.]]"},{"key":"e_1_2_1_57_1","first-page":"3","article-title":"Polymorphic type, region and effect inference","volume":"2","author":"Talpin J.-P.","year":"1992","unstructured":"Talpin , J.-P. and Jouvelot , P. 1992 . Polymorphic type, region and effect inference . J. Funct. Prog. 2 , 3 (July), 245--272.]] Talpin, J.-P. and Jouvelot, P. 1992. Polymorphic type, region and effect inference. J. Funct. Prog. 2, 3 (July), 245--272.]]","journal-title":"J. Funct. Prog."},{"key":"e_1_2_1_58_1","volume-title":"International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP '96)","volume":"1140","author":"Thiemann P.","year":"1996","unstructured":"Thiemann , P. 1996 . Implementing memoization for partial evaluation . In International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP '96) (Aachen, Germany), H. Kuchen and D. Swierstra, Eds. Lecture Notes in Computer Science , vol. 1140 . Springer-Verlag, New York, 198--212.]] Thiemann, P. 1996. Implementing memoization for partial evaluation. In International Symposium on Programming Languages, Implementations, Logics and Programs (PLILP '96) (Aachen, Germany), H. Kuchen and D. Swierstra, Eds. Lecture Notes in Computer Science, vol. 1140. Springer-Verlag, New York, 198--212.]]"},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the 1997 Conference on Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science","volume":"6","author":"Thiemann P.","year":"1997","unstructured":"Thiemann , P. 1997 a. Correctness of a region-based binding-time analysis . In Proceedings of the 1997 Conference on Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science , vol. 6 . Carnegie Mellon University, Pittsburgh, Pa. Elsevier Science, BV, Amsterdam, The Netherlands. URL: http:\/\/www.elsevier.nl\/ locate\/entcs\/volume6.html.]] Thiemann, P. 1997a. Correctness of a region-based binding-time analysis. In Proceedings of the 1997 Conference on Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol. 6. Carnegie Mellon University, Pittsburgh, Pa. Elsevier Science, BV, Amsterdam, The Netherlands. URL: http:\/\/www.elsevier.nl\/ locate\/entcs\/volume6.html.]]"},{"key":"e_1_2_1_60_1","series-title":"Lecture Notes in Computer Science","volume-title":"TAPSOFT '97: Theory and Practice of Software Development","author":"Thiemann P.","unstructured":"Thiemann , P. 1997b. A unified framework for binding-time analysis . In TAPSOFT '97: Theory and Practice of Software Development , M. Bidoit and M. Dauchet, Eds. Number 1214 in Lecture Notes in Computer Science . Springer-Verlag , Lille, France , 742--756.]] Thiemann, P. 1997b. A unified framework for binding-time analysis. In TAPSOFT '97: Theory and Practice of Software Development, M. Bidoit and M. Dauchet, Eds. Number 1214 in Lecture Notes in Computer Science. Springer-Verlag, Lille, France, 742--756.]]"},{"key":"e_1_2_1_61_1","volume-title":"Proceedings of the 7th European Symposium on Programming","author":"Thiemann P.","year":"1998","unstructured":"Thiemann , P. 1998 . A generic framework for specialization . In Proceedings of the 7th European Symposium on Programming ( Lisbon, Portugal), C. Hankin, Ed. Lecture Notes in Computer Science, vol 1381. Springer-Verlag, New York, 267--281.]] Thiemann, P. 1998. A generic framework for specialization. In Proceedings of the 7th European Symposium on Programming (Lisbon, Portugal), C. Hankin, Ed. Lecture Notes in Computer Science, vol 1381. Springer-Verlag, New York, 267--281.]]"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003469"},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation PEPM '99 (San Antonio, Tex.), O. Danvy, Ed. ACM","author":"Thiemann P.","year":"1999","unstructured":"Thiemann , P. 1999 b. Interpreting specialization in type theory . In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation PEPM '99 (San Antonio, Tex.), O. Danvy, Ed. ACM , New York, 30--43. BRICS Notes Series NS-99-1.]] Thiemann, P. 1999b. Interpreting specialization in type theory. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation PEPM '99 (San Antonio, Tex.), O. Danvy, Ed. ACM, New York, 30--43. BRICS Notes Series NS-99-1.]]"},{"key":"e_1_2_1_64_1","volume-title":"The PGG System--User Manual. Universit\u00e4t Freiburg","author":"Thiemann P.","unstructured":"Thiemann , P. 2000. The PGG System--User Manual. Universit\u00e4t Freiburg , Freiburg, Germany . Available from http:\/\/www.informatik.uni-freiburg.de\/proglang\/software\/pgg\/.]] Thiemann, P. 2000. The PGG System--User Manual. Universit\u00e4t Freiburg, Freiburg, Germany. Available from http:\/\/www.informatik.uni-freiburg.de\/proglang\/software\/pgg\/.]]"},{"key":"e_1_2_1_65_1","volume-title":"Proceedings of the 2001 European Symposium on Programming","author":"Thiemann P.","year":"2001","unstructured":"Thiemann , P. 2001 . Enforcing safety properties using type specialization . In Proceedings of the 2001 European Symposium on Programming ( Genova,Italy), D. Sands, Ed. Lecture Notes in Computer Science. Springer-Verlag, New York.]] Thiemann, P. 2001. Enforcing safety properties using type specialization. In Proceedings of the 2001 European Symposium on Programming (Genova,Italy), D. Sands, Ed. Lecture Notes in Computer Science. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the 11th European Symposium on Programming","volume":"2305","author":"Thiemann P.","year":"2002","unstructured":"Thiemann , P. 2002 . A prototype dependency calculus . In Proceedings of the 11th European Symposium on Programming ( Grenoble, France), D. L. Metay\u00e8r, Ed. Lecture Notes in Computer Science , vol. 2305 . Springer-Verlag, New York, 228--242.]] Thiemann, P. 2002. A prototype dependency calculus. In Proceedings of the 11th European Symposium on Programming (Grenoble, France), D. L. Metay\u00e8r, Ed. Lecture Notes in Computer Science, vol. 2305. Springer-Verlag, New York, 228--242.]]"},{"key":"e_1_2_1_67_1","unstructured":"Thiemann P. and Dussart D. 1997. Partial evaluation for higher-order languages with state. Berichte des Wilhelm-Schickard-Instituts WSI-97-XX Universit\u00e4t T\u00fcbingen. Apr.]] Thiemann P. and Dussart D. 1997. Partial evaluation for higher-order languages with state. Berichte des Wilhelm-Schickard-Instituts WSI-97-XX Universit\u00e4t T\u00fcbingen. Apr.]]"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/291891.291894"},{"key":"e_1_2_1_69_1","doi-asserted-by":"crossref","unstructured":"Tofte M. and Birkedal L. 2000. Unification and polymorphism in region inference. In Proof Language and Interaction: Essays in Honour of Robin Milner. MIT Press Cambridge Mass.]] Tofte M. and Birkedal L. 2000. Unification and polymorphism in region inference. In Proof Language and Interaction: Essays in Honour of Robin Milner. MIT Press Cambridge Mass.]]","DOI":"10.7551\/mitpress\/5641.003.0020"},{"issue":"0","key":"e_1_2_1_70_1","first-page":"0","article-title":"Programming with Regions in the ML Kit","volume":"4","author":"Tofte M.","year":"2001","unstructured":"Tofte , M. , Birkedal , L. , Elsman , M. , Hallenberg , N. , Olensen , T. , and Sestoft , P. 2001 . Programming with Regions in the ML Kit , Version 4 . 0 . 0 . Available from http:\/\/www.it.edu\/research\/ mlkit\/dist\/mlkit-4.0.0.pdf.]] Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N., Olensen, T., and Sestoft, P. 2001. Programming with Regions in the ML Kit, Version 4.0.0. Available from http:\/\/www.it.edu\/research\/ mlkit\/dist\/mlkit-4.0.0.pdf.]]","journal-title":"Version"},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the 1994 ACM SIGPLAN Symposium on Principles of Programming Languages (Portland, Ore). ACM","author":"Tofte M.","unstructured":"Tofte , M. and Talpin , J . -P. 1994. Implementation of the typed call-by-value \u03bb-calculus using a stack of regions . In Proceedings of the 1994 ACM SIGPLAN Symposium on Principles of Programming Languages (Portland, Ore). ACM , New York, 188--201.]] 10.1145\/174675.177855 Tofte, M. and Talpin, J.-P. 1994. Implementation of the typed call-by-value \u03bb-calculus using a stack of regions. In Proceedings of the 1994 ACM SIGPLAN Symposium on Principles of Programming Languages (Portland, Ore). ACM, New York, 188--201.]] 10.1145\/174675.177855"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1011508.1011510","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1011508.1011510","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:25:42Z","timestamp":1750281942000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1011508.1011510"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,7]]},"references-count":67,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,7]]}},"alternative-id":["10.1145\/1011508.1011510"],"URL":"https:\/\/doi.org\/10.1145\/1011508.1011510","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,7]]},"assertion":[{"value":"2004-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}