{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:56Z","timestamp":1725664976673},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631651"},{"type":"electronic","value":"9783540691945"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63165-8_181","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:10:38Z","timestamp":1330297838000},"page":"237-247","source":"Crossref","is-referenced-by-count":1,"title":["On modular properties of higher order extensional lambda calculi"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neil","family":"Ghani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Y. 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":"23_CR2","unstructured":"F. Barbanera. Combining term-rewriting and type-assignment systems. In Third Italian Conference on Theoretical Computer Science, Mantova, 1989. World Scientific Publishing Company."},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1142\/S0129054190000138","volume":"1","author":"F. Barbanera","year":"1990","unstructured":"F. Barbanera. Combining term rewriting and type assignment systems. Int. Journal of Found. of Comp. Science, 1:165\u2013184, 1990.","journal-title":"Int. Journal of Found. of Comp. Science"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"F. Barbanera and M. Fernandez. Intersection type assignment systems with higher-order algebraic rewriting. Theoretical Computer Science. To appear.","DOI":"10.1016\/S0304-3975(96)80706-7"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"F. Barbanera and M. Fernandez. Modularity of termination and confluence in combinations of rewrite systems with \u03bb \u03c9 . In A.Lingas, R.Karlsson, and S.Carlsson, editors, Intern. Conf. on Automata, Languages and Programming (ICALP), number 700 in Lecture Notes in Computer Science, Lund, 1993.","DOI":"10.1007\/3-540-56939-1_110"},{"key":"23_CR6","unstructured":"F. Barbanera and M. Fernandez. Modularity of termination and confluence in combinations of rewrite systems with the typed lambda-calculus of order omega. Technical report, Universit Paris Sud, 1994."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fernandez, and H. Geuvers. Modularity of strong normalization and confluence in the algebraic-\u03bb-cube. In Proceedings of the Symposium on Logic in Computer Science (LICS), Paris, 1994. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1994.316049"},{"key":"23_CR8","unstructured":"H. Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984."},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher order types. In IEEE, editor, Proceedings of the Symposium on Logic in Computer Science (LICS), pages 82\u201390, July 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"23_CR10","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. Theoretical Computer Science, 83:3\u201328, 1991.","journal-title":"Theoretical Computer Science"},{"key":"23_CR11","doi-asserted-by":"crossref","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. Information and Computation. 114:1\u201329, 1994.","journal-title":"Information and Computation"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"T. Coquand and G. Huet. Constructions: a higher-order proof system for mechanizing mathematics. EUROCAL85 in LNCS 203, 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"23_CR13","unstructured":"D. Cubric. On free CCC. Distributed on the types mailing list, 1992."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of theoretical computer science, volume Vol. B: Formal Models and Semantics, chapter 6, pages 243\u2013320. The MIT Press, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"23_CR15","unstructured":"R. Di Cosmo. A brief history of rewriting with extensionality. In Kluwer, editor, Proceedings ofthe 1996 Glasgow Summer School, 1996. To appear. A set of slides is availables from http:\/\/www.dmi.ens.fr\/\u223cdicsmo."},{"key":"23_CR16","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. 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":"23_CR17","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D, Kesner. Combining algebraic rewriting, extensional lambda calculi and fixpoints. Theoretical Computer Science, 1995. To appear.","DOI":"10.1016\/S0304-3975(96)00121-1"},{"issue":"2","key":"23_CR18","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","volume":"101","author":"D. J. Dougherty","year":"1992","unstructured":"D. J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101(2):251\u2013267, Dec. 1992.","journal-title":"Information and Computation"},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"D. J. Dougherty. Some lambda calculi with categor\u00edcal 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":"23_CR20","unstructured":"G. Dowek,G. Huet, and B. Werner. On the definition of the eta-long normal form in the type systems of the cube. In Informal Proceedings of the Workshop \u201cTypes\u201d, Nijmegen, 1993."},{"key":"23_CR21","unstructured":"J. Gallier. On Girard's \u201cCandidats de Reductibilit\u00e9\u201d, pages 123\u2013203. Logic and Computer Science. Academic Press, 1990. Odifreddi, editor."},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"N. Ghani. Eta-expansions in dependent type theory \u2014 the calculus of constructions. In Proceedings, TLCA 97 LNCS 1210, Nancy, France 1997. Eds de Groote and JR Hindley","DOI":"10.1007\/3-540-62688-3_35"},{"key":"23_CR23","unstructured":"N. Ghani. Eta-expansions in F \u03c9 . Presented at CSL'96 Utrecht Holland. To appear in CSL'96 proceedings."},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"N. Ghani. \u03b2\u03b7-equality for coproducts. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, Apr. 1995.","DOI":"10.1007\/BFb0014052"},{"key":"23_CR25","unstructured":"N. Ghani. Extensionality and polymorphism. University of Edimburgh, Submitted, 1995."},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"B. Howard and J. Mitchell. Operational and axiomatic semantics of pcf. In Proceedings of the LISP and Functional Programming Conference, pages 298\u2013306. ACM, 1990.","DOI":"10.1145\/91556.91677"},{"key":"23_CR27","unstructured":"C. B. Jay and N. Ghani. The Virtues of Eta-expansion. Technical Report ECS-LFCS-92-243, LFCS, 1992. University of Edimburgh. preliminary version of [28]."},{"issue":"2","key":"23_CR28","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C. B. Jay","year":"1995","unstructured":"C. B. Jay and N. Ghani. The Virtues of Eta-expansion. Journal of Functional Programming, 5(2):135\u2013154, Apr. 1995.","journal-title":"Journal of Functional Programming"},{"key":"23_CR29","first-page":"350","volume-title":"A computation model for executable higher-order algebraic specification languages","author":"J.-P. Jouannaud","year":"1991","unstructured":"J.-P. Jouannaud and M. 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, 15\u201318 July 1991. IEEE Computer Society Press."},{"key":"23_CR30","unstructured":"G. Mints. Teorija categorii i teoria dokazatelstv.I. Aktualnye problemy logiki i metodologii nauky, pages 252\u2013278, 1979."},{"key":"23_CR31","unstructured":"V. van Oostrom. Developing developments. Submitted to Theoretical Computer Science should appear in volume 145, 1994."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63165-8_181.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:16:23Z","timestamp":1605647783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63165-8_181"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631651","9783540691945"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-63165-8_181","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}