{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:16Z","timestamp":1742617216867,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_40","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:35:42Z","timestamp":1330292142000},"page":"215-232","source":"Crossref","is-referenced-by-count":5,"title":["Rewriting with extensional polymorphic \u03bb-calculus"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Yohji Akama. On Mints' reductions for ccc-Calculus. In Typed Lambda Calculus and Applications, number 664 in LNCS, pages 1\u201312. Springer Verlag, 1993.","DOI":"10.1007\/BFb0037094"},{"key":"13_CR2","unstructured":"Henk Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984."},{"key":"13_CR3","first-page":"82","volume-title":"Combining algebra and higher-order types","author":"V. Breazu-Tannen","year":"1988","unstructured":"Val Breazu-Tannen, Combining algebra and higher-order types. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 82\u201390, Edinburgh, Scotland, July 5\u20138 1988. IEEE Computer Society."},{"key":"13_CR4","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. Polymorphic rewiting preserves algebraic confluence. Information and Computation, 114:1\u201329, 1994.","journal-title":"Information and Computation"},{"key":"13_CR5","first-page":"7","volume-title":"Polymorphism is conservative over simple types (preliminary report)","author":"V. Breazu-Tannen","year":"1986","unstructured":"Val Breazu-Tannen and Albert R. Meyer. Polymorphism is conservative over simple types (preliminary report). In Proceedings, Symposium on Logic in Computer Science, pages 7\u201317, Cambridge, Massachusetts, June 16\u201318 1986. IEEE Computer Society."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the \u03bb-calculus with surjective pairing and terminal object. In Leach, Monien, and Artalejo, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 510 of Lecture Notes in Computer Science, pages 291\u2013302. Springer-Verlag, July 1991.","DOI":"10.1007\/3-540-54233-7_142"},{"key":"13_CR7","unstructured":"Djordje Cubric. On free CCC. Distributed on the types mailing list, 1992."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Roberto Di Cosmo and Delia Kesner. Combining first order algebraic rewriting systems, recursion and extensional lambda calculi. In Serge Abite-boul and Eli Shamir, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), volume 820 of Lecture Notes in Computer Science, pages 462\u2013472. Springer-Verlag, July 1994.","DOI":"10.1007\/3-540-58201-0_90"},{"key":"13_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129500000359","volume":"4","author":"R. Cosmo Di","year":"1994","unstructured":"Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1\u201348, 1994. A preliminary version is available as Technical Report LIENS-93-11\/INRIA 1911.","journal-title":"Mathematical Structures in Computer Science"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Roberto Di Cosmo and Adolfo Piperno. Expanding extensional polymorphism. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 139\u2013153, April 1995.","DOI":"10.1007\/BFb0014050"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Daniel J. Dougherty. Some lambda calculi with categorical sums and products. In Proc, of the Fifth International Conference on Rewriting Techniques and Applications (RTA), 1993.","DOI":"10.1007\/3-540-56868-9_12"},{"key":"13_CR12","unstructured":"Alfons Geser. Relative termination. Dissertation, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau, Germany, 1990. Also available as: Report 91-03, Ulmer Informatik-Berichte, Universit\u00e4t Ulm, 1991."},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Herman Geuvers. The church-rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In 7th Proceedings of the Symposium on Logic in Computer Science (LICS), pages 453\u2013460, 1992.","DOI":"10.1109\/LICS.1992.185556"},{"key":"13_CR14","unstructured":"Neil Ghani. Extensionality and polymorphism. University of Edimburgh, Submitted, 1995."},{"key":"13_CR15","unstructured":"Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge University Press, 1990."},{"key":"13_CR16","unstructured":"Colin Barry Jay. Long \u03b2\u03b7 normal forms and confluence (revised). Technical Report 44, LFCS \u2014 University of Edinburgh, August 1992."},{"key":"13_CR17","unstructured":"Colin Barry Jay and Neil Ghani. The Virtues of Eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh, preliminary version of [JG95]."},{"issue":"2","key":"13_CR18","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C. B. Jay","year":"1995","unstructured":"Colin Barry Jay and Neil Ghani. The Virtues of Eta-expansion. Journal of Functional Programming, 5(2):135\u2013154, April 1995.","journal-title":"Journal of Functional Programming"},{"key":"13_CR19","first-page":"350","volume-title":"A computation model for executable higher-order algebraic specification languages","author":"J. Jouannaud","year":"1991","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 350\u2013361, Amsterdam, The Netherlands, July 15\u201318 1991. IEEE Computer Society Press."},{"key":"13_CR20","unstructured":"Jan Willem Klop. Combinatory reduction systems. Mathematical Center Tracts, 27, 1980."},{"key":"13_CR21","unstructured":"Tobias Nipkow. A critical pair lemma for higher-order rewrite systems and its application to \u03bb*. First Annual Workshop on Logical Frameworks, 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:18:34Z","timestamp":1742599114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}