{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T20:16:00Z","timestamp":1768680960374,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540543961","type":"print"},{"value":"9783540475996","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3540543961_22","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:44:08Z","timestamp":1330209848000},"page":"448-472","source":"Crossref","is-referenced-by-count":52,"title":["Efficient type inference for higher-order binding-time analysis"],"prefix":"10.1007","author":[{"given":"Fritz","family":"Henglein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,7,6]]},"reference":[{"key":"22_CR1","unstructured":"A. Aho, J. Hopcroft, and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974."},{"key":"22_CR2","unstructured":"A. Aho, R. Sethi, and J. Ullman. Compilers: Principles, Techniques, and Tools. Addison Wesley, 1986. Addison-Wesley, 1986, Reprinted with corrections, March 1988."},{"key":"22_CR3","unstructured":"A. Bondorf, N. Jones, T. Mogensen, and P. Sestoft. Binding time analysis and the taming of self-application. Sep. 1988. To appear in Transactions on Programming Languages and Systems (TOPLAS)."},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"A. Bondorf. Automatic autoprojection of higher order recursive equations. In N. Jones, editor, Proc. 3rd European Symp. on Programming (ESOP '90), Copenhagen, Denmark, pages 70\u201387, Springer, May 1990. Lecture Notes in Computer Science, Vol. 432.","DOI":"10.1007\/3-540-52592-0_56"},{"key":"22_CR5","unstructured":"A. Bondorf. Self-Applicable Partial Evaluation. PhD thesis, DIKU, University of Copenhagen, Dec. 1990."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"C. Consel. New insights into partial evaluation: the Schism experiment. In Proc. 2nd European Symp. on Programming (ESOP), Nancy, France, pages 236\u2013246, Springer, 1988. Lecture Notes in Computer Science, Vol. 300.","DOI":"10.1007\/3-540-19027-9_16"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"C. Consel. Binding time analysis for higher order untyped functional languages. In Proc. LISP and Functional Programmin (LFP), Nice, France, ACM, July 1990.","DOI":"10.1145\/91556.91668"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Y. Fuh and P. Mishra. Type inference with subtypes. In Proc. 2nd European Symp. on Programming, pages 94\u2013114, Springer-Verlag, 1988. Lecture Notes in Computer Science 300.","DOI":"10.1007\/3-540-19027-9_7"},{"issue":"1","key":"22_CR9","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1017\/S0956796800000058","volume":"1","author":"C. Gomard","year":"1991","unstructured":"C. Gomard and N. Jones. A partial evaluator for the untyped lambda-calculus. J. Functional Programming, 1(1):21\u201369, Jan. 1991.","journal-title":"J. Functional Programming"},{"key":"22_CR10","volume-title":"Higher Order Partial Evaluation \u2014 HOPE for the Lambda Calculus","author":"C. Gomard","year":"1989","unstructured":"C. Gomard. Higher Order Partial Evaluation \u2014 HOPE for the Lambda Calculus. Master's thesis, DIKU, University of Copenhagen, Denmark, September 1989."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"C. Gomard. Partial type inference for untyped functional programs (extended abstract). In Proc. LISP and Functional Programming (LFP), Nice, France, July 1990.","DOI":"10.1145\/91556.91672"},{"key":"22_CR12","unstructured":"F. Henglein. Simple type inference and unification. Oct. 1988. New York University, Computer Science Department, SETL Newsletter 232."},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"F. Henglein. Type inference and semi-unification. In Proc. ACM Conf. on LISP and Functional Programming (LFP), Snowbird, Utah, pages 184\u2013197, ACM, ACM Press, July 1988.","DOI":"10.1145\/62678.62701"},{"key":"22_CR14","unstructured":"F. Henglein. Dynamic typing. March 1991. Semantique note 90, DIKU, University of Copenhagen."},{"key":"22_CR15","unstructured":"J. Hopcroft and R. Karp. An Algorithm for Testing the Equivalence of Finite Automata. Technical Report TR-71-114, Dept. of Computer Science, Cornell U., 1971."},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"S. Hunt and D. Sands. Binding time analysis: a new PERspective. In Proc. ACM\/IFIP Symp. on Partial Evaluation and Semantics Based Program Manipulation (PEPM), New Haven, Connecticut, June 1991.","DOI":"10.1145\/115865.115881"},{"key":"22_CR17","unstructured":"G. Huet. R\u00e9solution d'equations dans des langages d'ordre 1, 2, ..., omega. PhD thesis, Univ. Paris VII, Sept. 1976."},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"N. Jones, C. Gomard, A. Bondorf, O. Danvy, and T. Mogensen. A self-applicable partial evaluator for the lambda calculus. In 1990 International Conference on Computer Languages, New Orleans, Louisiana, March 1990, pages 49\u201358, IEEE Computer Society, 1990.","DOI":"10.1109\/ICCL.1990.63760"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"N. Jones and S. Muchnick. Binding time optimization in programming languages: some thoughts toward the design of the ideal language. In Proc. 3rd ACM Symp. on Principles of Programming Languages, pages 77\u201394, ACM, Jan. 1976.","DOI":"10.1145\/800168.811542"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"N. Jones and S. Muchnick. TEMPO: A Unified Treatment of Binding Time and Parameter Passing Concepts in Programming Languages. Volume 66 of Lecture Notes in Computer Science, Springer, 1978.","DOI":"10.1007\/3-540-09085-1"},{"key":"22_CR21","unstructured":"N. Jones. Automatic program specialization: a re-examination from basic principles. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Partial Evaluation and Mixed Computation, pages 225\u2013282, IFIP, North-Holland, Oct. 1987."},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"N. Jones and D. Schmidt. Compiler generation from denotational semantics. In N. Jones, editor, Semantics-Directed Compiler Generation, Aarhus, Denmark, pages 70\u201393, Springer, 1980. Lecture Notes in Computer Science, Vol. 94.","DOI":"10.1007\/3-540-10250-7_19"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"N. Jones, P. Sestoft, and H. Sondergard. An experiment in partial evaluation: the generation of a compiler generator. SIGPLAN Notices, 20(8), Aug. 1985.","DOI":"10.1145\/988346.988358"},{"key":"22_CR24","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01806312","volume":"2","author":"N. Jones","year":"1989","unstructured":"N. Jones, P. Sestoft, and H. Sondergaard. Mix: a self-applicable partial evaluator for experiments in compiler generation. LISP and Symbolic Computation, 2:9\u201350, 1989.","journal-title":"LISP and Symbolic Computation"},{"key":"22_CR25","first-page":"20","volume-title":"GI \u2014 11. Jahrestagung, Munich, Germany","author":"H. Kr\u00f6ger","year":"1981","unstructured":"H. Kr\u00f6ger. Static-Scope-Lisp: splitting an interpreter into compiler and run-time system. In W. Brauer, editor, GI \u2014 11. Jahrestagung, Munich, Germany, pages 20\u201331, Springer, Munich, Germany, 1981. Informatik-Fachberichte 50."},{"key":"22_CR26","unstructured":"J. Launchbury. Projections for specialisation. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 465\u2013483, North-Holland, Oct. 1987."},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"J. Launchbury. Projection Factorisations in Partial Evaluation. PhD thesis, University of Glasgow, Jan. 1990.","DOI":"10.1017\/CBO9780511569814"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"J. Lassez, M. Maher, and K. Marriott. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, Morgan Kauffman, 1987.","DOI":"10.1016\/B978-0-934613-40-8.50019-1"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"J. Mitchell. Coercion and type inference. In Proc. 11th ACM Symp. on Principles of Programming Languages (POPL), 1984.","DOI":"10.1145\/800017.800529"},{"issue":"2","key":"22_CR30","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258\u2013282, Apr. 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR31","unstructured":"T. Mogensen. Partially static structures in a self-applicable partial evaluator. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 325\u2013347, North-Holland, Oct. 1987."},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"T. Mogensen. Binding time analysis for polymorphically typed higher order languages. In J. Diaz and F. Orejas, editors, Proc. Int. Conf. Theory and Practice of Software Development (TAPSOFT), Barcelona, Spain, pages 298\u2013312, Springer, March 1989. Lecture Notes in Computer Science 352.","DOI":"10.1007\/3-540-50940-2_43"},{"key":"22_CR33","doi-asserted-by":"crossref","unstructured":"H. Nielson and F. Nielson. Semantics directed compiling for functional languages. In Proc. ACM Conf. on LISP and Functional Programming (LFP), 1986.","DOI":"10.1145\/319838.319867"},{"key":"22_CR34","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0167-6423(88)90025-1","volume":"10","author":"H. Nielson","year":"1988","unstructured":"H. Nielson and F. Nielson. Automatic binding time analysis for a typed lambda calculus. Science of Computer Programming, 10:139\u2013176, 1988.","journal-title":"Science of Computer Programming"},{"key":"22_CR35","doi-asserted-by":"crossref","unstructured":"H. Nielson and F. Nielson. Two-level semantics and code generation. Theoretical Computer Science, 56, 1988.","DOI":"10.1016\/0304-3975(86)90006-X"},{"key":"22_CR36","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. Paterson","year":"1978","unstructured":"M. Paterson and M. Wegman. Linear unification. J. Computer and System Sciences, 16:158\u2013167, 1978.","journal-title":"J. Computer and System Sciences"},{"key":"22_CR37","unstructured":"S. Romanenko. A compiler generator produced by a self-applicable specializer can have a surprisingly natural and understandable structure. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 465\u2013483, North-Holland, Oct. 1987."},{"key":"22_CR38","unstructured":"D. Schmidt. Static properties of partial evaluation. In D. Bjorner, A. Ershov, and N. Jones, editors, Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, pages 465\u2013483, North-Holland, Oct. 1987."},{"key":"22_CR39","doi-asserted-by":"crossref","unstructured":"P. Sestoft. The structure of a self-applicable partial partial evaluator. In H. Ganzinger and N. Jones, editors, Programs as Data Objects, Copenhagen, Denmark, pages 236\u2013256, Springer, 1985. published in 1986, Lecture Notices in Computer Science, Vol. 217.","DOI":"10.1007\/3-540-16446-4_14"},{"key":"22_CR40","first-page":"88","volume-title":"Proc. 15th ACM Symp. on Principles of Programming Languages","author":"R. Stansifer","year":"1988","unstructured":"R. Stansifer. Type inference with subtypes. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 88\u201397, ACM, San Diego, California, Jan. 1988."},{"key":"22_CR41","doi-asserted-by":"crossref","unstructured":"R. Tarjan. Depth-first search and linear graph algorithms. SIAM J. Comput., 1(2), June 1972.","DOI":"10.1137\/0201010"},{"key":"22_CR42","doi-asserted-by":"crossref","unstructured":"R. Tarjan. Data Structures and Network Flow Algorithms. Volume CMBS 44 of Regional Conference Series in Applied Mathematics, SIAM, 1983.","DOI":"10.1137\/1.9781611970265"},{"key":"22_CR43","doi-asserted-by":"crossref","first-page":"115","DOI":"10.3233\/FI-1987-10202","volume":"X","author":"M. Wand","year":"1987","unstructured":"M. Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, X:115\u2013122, 1987.","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Functional Programming Languages and Computer Architecture"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3540543961_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T03:45:01Z","timestamp":1640922301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3540543961_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540543961","9783540475996"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/3540543961_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991]]}}}