{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:31Z","timestamp":1725664711416},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540630456"},{"type":"electronic","value":"9783540690658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63045-7_40","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:00:46Z","timestamp":1330279246000},"page":"399-409","source":"Crossref","is-referenced-by-count":1,"title":["Simulating \u03b7-expansions with \u0392-reductions in the second-order polymorphic \u03bb-rcalculus"],"prefix":"10.1007","author":[{"given":"Hongwei","family":"Xi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"40_CR1","first-page":"1","volume":"664","author":"Y. Akama","year":"1993","unstructured":"Y. Akama (1993), On Mints' reduction for ccc-calculus. In Typed lambda-calculi and applications, vol. 664 of LNCS, pp 1\u201312.","journal-title":"LNCS"},{"key":"40_CR2","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"H.P. Barendregt (1984), The Lambda Calculus: Its Syntax and Semantics, North-Holland publishing company, Amsterdam."},{"key":"40_CR3","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H.P. Barendregt","year":"1992","unstructured":"H.P. Barendregt (1992), Lambda calculi with types, Handbook of Logic in Computer Science edited by S. Abramsky, Dov M. Gabbay and T.S.E. Maibaum, Clarendon Press, Oxford, pp. 117\u2013414."},{"key":"40_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","volume":"83","author":"V. Breazu-Tannen","year":"1991","unstructured":"Val Breazu-Tannen and Jean Gallier (1991), Polymorphic rewriting conserves strong normalization, Theoretic Computer Sicence, vol. 83, pp 3\u201328.","journal-title":"Theoretic Computer Sicence"},{"issue":"1","key":"40_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1078","volume":"114","author":"V. Breazu-Tannen","year":"1994","unstructured":"Val Breazu-Tannen and Jean Gallier (1994), Polymorphic rewriting preserves algebraic confluence, Information and Computation, vol. 114(1), pp. 1\u201329.","journal-title":"Information and Computation"},{"key":"40_CR6","unstructured":"Djordje Cubric (1992), On free ccc, Manuscripts."},{"key":"40_CR7","first-page":"462","volume":"820","author":"R. Cosmo Di","year":"1994","unstructured":"R. Di Cosmo and D. Kesner (1994), Combining the first order algebraic rewriting systems, recursion and extensional lambda calculi. In Serge Abiteboul and Eli Shamir, editors, International Conference on Automata, Languages and Programming, vol. 820 of LNCS, pp. 462\u2013472.","journal-title":"LNCS"},{"key":"40_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129500000359","volume":"4","author":"R. Cosmo Di","year":"1994","unstructured":"R. Di Cosmo and D. Kesner (1994), Simulating expansions without expansions. Mathematical Structures in Computer Science, vol. 4, pp. 1\u201348.","journal-title":"Mathematical Structures in Computer Science"},{"key":"40_CR9","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1007\/3-540-61377-3_40","volume":"1092","author":"R. Cosmo Di","year":"1995","unstructured":"R. Di Cosmo and D. Kesner (1995), Rewriting with polymorphic extensional lambda-calculus. In Proceedings of Computer Science Logic '95, vol. 1092 of Lecture Notes in Computer Science, pages 215\u2013232.","journal-title":"Lecture Notes in Computer Science"},{"key":"40_CR10","first-page":"139","volume":"902","author":"R. Cosmo Di","year":"1995","unstructured":"R. Di Cosmo and A. Piperno (1995), Expanding Extensional Polymorphism, In Proceedings of Typed Lambda-Calculi and Applications, vol. 902 of LNCS, pp. 139\u2013153.","journal-title":"LNCS"},{"key":"40_CR11","doi-asserted-by":"crossref","unstructured":"Daniel J. Dougherty (1993), Some lambda calculi with categorical sums and products. In Proceedings of the 5th International Conference on Rewriting Techniques and Applications.","DOI":"10.1007\/3-540-56868-9_12"},{"key":"40_CR12","first-page":"171","volume":"902","author":"N. Ghani","year":"1995","unstructured":"N. Ghani (1995), \u0392\u03b7-equality for coproducts. In Typed lambda-calculi and applications, vol. 902 of LNCS, pp. 171\u2013185.","journal-title":"LNCS"},{"key":"40_CR13","doi-asserted-by":"crossref","unstructured":"N. Ghani (1996), Eta Expansions in System F, Manuscripts.","DOI":"10.1007\/3-540-63172-0_39"},{"key":"40_CR14","unstructured":"J.-Y. Girard (1972), Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se de doctorat d'etat, Universit\u00e9 Paris VII."},{"issue":"2","key":"40_CR15","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C.B. Jay","year":"1996","unstructured":"C.B. Jay and N. Ghani (1996), The virtues of eta-expansion, Journal of Functional Programming, vol. 5(2), pp. 135\u2013154.","journal-title":"Journal of Functional Programming"},{"key":"40_CR16","unstructured":"J. Lambek and P.J. Scott (1986), An introduction to higher order categorical logic, Cambridge University Press."},{"key":"40_CR17","unstructured":"G.E. Mints (1979), Theory of categories and theory of proofs (I). In Urgent Question of Logic and the Methodology of Science [In Russian], Kiev."},{"key":"40_CR18","volume-title":"Ideas and results of proof theory","author":"D. Prawitz","year":"1971","unstructured":"D. Prawitz (1971), Ideas and results of proof theory, Proceedings of the 2nd Scandinavia logic symposium, editor J.E. Fenstad, North-Holland Publishing Company, Amsterdam."},{"key":"40_CR19","first-page":"408","volume":"19","author":"J. Reynolds","year":"1974","unstructured":"J. Reynolds (1974), Towards a theory of type structure, Colloquium sur la Progrmmation, vol. 19 of LNCS, pp. 408\u2013423.","journal-title":"LNCS"},{"key":"40_CR20","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01621476","volume":"30","author":"H. Schwichtenberg","year":"1991","unstructured":"H. Schwichtenberg (1991), An upper bound for reduction sequences in the typed lambda-calculus, Archive for Mathematical Logic, 30:405\u2013408.","journal-title":"Archive for Mathematical Logic"},{"key":"40_CR21","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. Tait","year":"1967","unstructured":"W. Tait (1967), Intensional Interpretations of functionals of finite type I, J. symbolic logic 32, pp. 198\u2013212.","journal-title":"J. symbolic logic"},{"key":"40_CR22","volume-title":"Research Report 96-189","author":"H. Xi","year":"1996","unstructured":"H. Xi (1996), Upper bounds for standardizations and an application, Research Report 96-189, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh."},{"key":"40_CR23","volume-title":"Research Report","author":"H. Xi","year":"1996","unstructured":"H. Xi (1996), Simulating eta-expansions with beta-reductions in the secondorder polymorphic lambda-Calculus, Research Report, Department of Mathematical Sciences, Carnegie Mellon University, Pittsburgh. Available through pointer: http:\/\/www.cs.cmu.edu\/~hwxi\/papers\/EtaSim.ps"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63045-7_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:15:18Z","timestamp":1605629718000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63045-7_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540630456","9783540690658"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-63045-7_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}