{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:20:36Z","timestamp":1759638036860},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540513711"},{"type":"electronic","value":"9783540462019"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/bfb0035757","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T09:00:28Z","timestamp":1133427628000},"page":"137-150","source":"Crossref","is-referenced-by-count":13,"title":["Polymorphic rewriting conserves algebraic strong normalization and confluence"],"prefix":"10.1007","author":[{"given":"Val","family":"Breazu-Tannen","sequence":"first","affiliation":[]},{"given":"Jean","family":"Gallier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,11,29]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen and T. Coquand. Extensional models for polymorphism. Theoretical Computer Science, 85\u2013114, 1988.","DOI":"10.1016\/0304-3975(88)90097-7"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen and A. R. Meyer. Computable values can be classical. In Proceedings of the 14th Symposium on Principles of Programming Languages, pages 238\u2013245, ACM, January 1987.","DOI":"10.1145\/41625.41646"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of the Symposium on Logic in Computer Science, pages 82\u201390, IEEE, July 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"10_CR4","first-page":"95","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Control, 76:95\u2013120, 1988.","journal-title":"Information and Control"},{"key":"10_CR5","unstructured":"D. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Manuscript, Wesleyan University. March 1989."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of algebraic specification 1: equations and initial semantics. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"10_CR7","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"key":"10_CR8","unstructured":"J. Y. Girard, Y. Lafont, and P. Taylor. Typed lambda calculus. Cambridge University Press, 1989. Forthcoming."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"J. Gallier and W. Snyder. Complete sets of transformations for general E-Unification. Theoretical Computer Science, 1989. To appear.","DOI":"10.1016\/0304-3975(89)90004-2"},{"key":"10_CR10","unstructured":"J. Gallier and W. Snyder. Higher-order unification revisited: complete sets of transformations. Journal of Symbolic Computation, 1989. To appear."},{"key":"10_CR11","volume-title":"Combinatory reduction systems","author":"J. W. Klop","year":"1980","unstructured":"J. W. Klop. Combinatory reduction systems. Tract 129, Mathematical Center, Amsterdam, 1980."},{"key":"10_CR12","first-page":"143","volume":"32","author":"J. W. Klop","year":"1987","unstructured":"J. W. Klop. Term rewriting systems: a tutorial. Bull. EATCS, 32:143\u2013182, June 1987.","journal-title":"Bull. EATCS"},{"key":"10_CR13","series-title":"Technical Report","volume-title":"Deduction with many-sorted rewrite","author":"J. Meseguer","year":"1985","unstructured":"J. Meseguer and J. Goguen. Deduction with many-sorted rewrite. Technical Report 42, CSLI, Stanford, 1985."},{"key":"10_CR14","first-page":"308","volume-title":"Proceedings of the LISP and Functional Programming Conference","author":"J. C. Mitchell","year":"1986","unstructured":"J. C. Mitchell. A type-inference approach to reduction properties and semantics of polymorphic expressions. In Proceedings of the LISP and Functional Programming Conference, pages 308\u2013319, ACM, New York, August 1986."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"A. R. Meyer and M. B. Reinhold. \u2018Type\u2019 is not a type: preliminary report. In Conf. Record Thirteenth Ann. Symp. Principles of Programming Languages, pages 287\u2013295, ACM, January 1986.","DOI":"10.1145\/512644.512671"},{"key":"10_CR16","doi-asserted-by":"crossref","first-page":"17","DOI":"10.2307\/2273377","volume":"47","author":"R. Statman","year":"1982","unstructured":"R. Statman. Completeness, invariance and \u03bb-definability. Journal of Symbolic Logic, 47:17\u201326, 1982.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"R. Statman. Logical relations and the typed \u03bb-calculus. Information and Control, 65:85\u201397, 1985.","journal-title":"Information and Control"},{"key":"10_CR18","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait. Intensional interpretations of functionals of finite type i. Journal of Symbolic Logic, 32:198\u2013212, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"W. W. Tait. A realizability interpretation of the theoyr of species. In R. Parikh, editor, Proceedings of the Logic Colloqium '73, pages 240\u2013251, Lecture Notes in Mathematics, Vol. 453, Springer-Verlag, 1975.","DOI":"10.1007\/BFb0064875"},{"issue":"1","key":"10_CR20","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128\u2013143, January 1987.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0035757","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:31:32Z","timestamp":1586593892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035757"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540513711","9783540462019"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0035757","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}