{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:52Z","timestamp":1725664792610},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614647"},{"type":"electronic","value":"9783540685968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61464-8_53","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:39:38Z","timestamp":1330292378000},"page":"200-214","source":"Crossref","is-referenced-by-count":3,"title":["On the power of simple diagrams"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Y. Akama. On Mints' reductions for ccc-Calculus. In TLCA, n. 664 in LNCS, pages 1\u201312. Springer Verlag, 1993.","DOI":"10.1007\/BFb0037094"},{"key":"16_CR2","unstructured":"F. Barbanera. Combining term-rewriting and type-assignment systems. In 3rd It. Conf. on TCS, 1989."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fernandez, and H. Geuvers. Modularity of strong normalization and confluence in the algebraic-\u03bb-cube. In LICS, Paris, 1994.","DOI":"10.1109\/LICS.1994.316049"},{"key":"16_CR4","unstructured":"H. Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984."},{"key":"16_CR5","unstructured":"G. Bell\u00e8. Syntactical properties of an extension of girard's system f where types can be taken as \u201cgeneric\u201d inputs. 1995. Available as ftp:\/\/idefix.disi.unige.it\/pub\/gbelle\/systemFC.ps.Z."},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher order types. In LICS, pages 82\u201390, July 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","volume":"83","author":"V. Breazu-Tannen","year":"1991","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting preserves algebraic strong normalization. TCS, 83:3\u201328, 1991.","journal-title":"TCS"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1078","volume":"114","author":"V. Breazu-Tannen","year":"1994","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewiting preserves algebraic confluence. Inf. and Comp., 114:1\u201329, 1994.","journal-title":"Inf. and Comp."},{"key":"16_CR9","unstructured":"D. Cubric. On free CCC. Distributed on the types mailing list, 1992."},{"key":"16_CR10","unstructured":"P.-L. Curien and R. Di Cosmo. A confluent reduction system for the \u03bb-calculus with surjective pairing and terminal object. JFP, 1995. To appear. A preliminary version appeared in ICALP 91."},{"key":"16_CR11","first-page":"1","volume":"4","author":"R. Cosmo Di","year":"1994","unstructured":"R. Di Cosmo and D. Kesner. Simulating expansions without expansions. MSCS, 4:1\u201348, 1994.","journal-title":"MSCS"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Combining algebraic rewriting, extensional lambda calculi and fixpoints. TCS, 1995. To appear.","DOI":"10.1016\/S0304-3975(96)00121-1"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Rewriting with polymorphic extensional \u03bb-calculus. In CSL'95 (extended abstract), 1995. Full version accepted for CSL95 Proceedings, to appear in 1996.","DOI":"10.1007\/3-540-61377-3_40"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and A. Piperno. Expanding extensional polymorphism. In M. Dezani-Ciancaglini and G. Plotkin, editors, TLCA, volume 902 of LNCS, pages 139\u2013153, Apr. 1995.","DOI":"10.1007\/BFb0014050"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"D. J. Dougherty. Some lambda calculi with categorical sums and products. In RTA, 1993.","DOI":"10.1007\/3-540-56868-9_12"},{"key":"16_CR16","unstructured":"J. Gallier. On Girard's \u201cCandidats de Reductibilit\u00e9\u201d, pages 123\u2013203. Logic and Computer Science. Academic Press, 1990."},{"key":"16_CR17","volume-title":"Dissertation","author":"A. Geser","year":"1990","unstructured":"A. Geser. Relative termination. Dissertation, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Universit\u00e4t Passau, Germany, 1990."},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"N. Ghani. \u03b2\u03b7-equality for coproducts. In M. Dezani-Ciancaglini and G. Plotkin, editors, TLCA, volume 902 of LNCS, 1995.","DOI":"10.1007\/BFb0014052"},{"key":"16_CR19","unstructured":"N. Ghani. Extensionality and polymorphism. University of Edimburgh, Submitted, 1995."},{"key":"16_CR20","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1990."},{"key":"16_CR21","unstructured":"G. Huet R\u00e9solution d'\u00e9quations dans les langages d'ordre 1, 2,..., \u03c9. Th\u00e8se d'Etat, Universit\u00e9 Paris VII, 1976."},{"issue":"2","key":"16_CR22","first-page":"135","volume":"5","author":"C. B. Jay","year":"1995","unstructured":"C. B. Jay and N. Ghani. The Virtues of Eta-expansion. JFP, 5(2):135\u2013154, Apr. 1995.","journal-title":"JFP"},{"key":"16_CR23","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0304-3975(93)90093-9","volume":"121","author":"G. Longo","year":"1993","unstructured":"G. Longo, K. Milsted, and S. Soloviev. The Genericity Theorem and effective Parametricity in Polymorphic lambdacalculus. TCS, 121:323\u2013349, 1993.","journal-title":"TCS"},{"key":"16_CR24","unstructured":"G. Mints. Teorija categorii i teoria dokazatelstv.I. Aktualnye problemy logiki i metodologii nauky, pages 252\u2013278, 1979."},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"M. Okada. Strong normalizability for the combined system of the types lambda calculus and an arbitrary convergent term rewrite system. In Symp. Symb. and Alg. Comp., 1989.","DOI":"10.1145\/74540.74582"},{"key":"16_CR26","unstructured":"V. Tannen, P. Buneman, and L. Wong. Naturally embedded query languages. In 4th Int. Conf. on Database Theory, n. 646 in LNCS, 1992. Available as ftp:\/\/www.cis.upenn.edu\/pub\/papers\/db-research\/icdt92.dvi.Z."},{"key":"16_CR27","unstructured":"V. van Oostrom. Developing developments. Draft, 1994."},{"key":"16_CR28","unstructured":"L. Wong. Querying nested collections. PhD thesis, University of Pennsylvania, 1994. Available as ftp:\/\/www.cis.upenn.edu\/pub\/papers\/db-research\/limsoonphd.ps.Z."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61464-8_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:35:27Z","timestamp":1640946927000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}