{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T00:10:08Z","timestamp":1742602208633,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540626886"},{"type":"electronic","value":"9783540684381"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62688-3_35","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:48:23Z","timestamp":1330296503000},"page":"164-180","source":"Crossref","is-referenced-by-count":11,"title":["Eta-expansions in dependent type theory \u2014 The calculus of constructions"],"prefix":"10.1007","author":[{"given":"Neil","family":"Ghani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Y. Akama. On Mints' reduction for ccc-calculus. In Typed \u03bb-Calculus and Applications, volume 664 of Lecture Notes in Computer Science, pages 1\u201312. Springer Verlag, 1993.","DOI":"10.1007\/BFb0037094"},{"issue":"2\u20133","key":"11_CR2","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2\u20133):173\u2013202, October 1989.","journal-title":"Theoretical Computer Science"},{"key":"11_CR3","unstructured":"R. Di Cosmo. On the power of simple diagrams. To appear in RTA'96."},{"key":"11_CR4","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.","journal-title":"Mathematical Structures in Computer Science"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Combining algebraic rewriting, extensional \u03bb-calculi and fixpoints. In TCS, 1995.","DOI":"10.1016\/S0304-3975(96)00121-1"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"D. Dougherty. Some \u03bb-calculi with categorical sums and products. In Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 137\u2013151. Springer Verlag, 1993.","DOI":"10.1007\/3-540-56868-9_12"},{"key":"11_CR7","unstructured":"G. Dowek. On the defintion of the \u03b7-long normal form in type systems of the cube. Informal proceedings of the 1993 Workshop on Types for Proofs and Programs, 1993."},{"key":"11_CR8","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":"11_CR9","doi-asserted-by":"crossref","unstructured":"H. Geuvers. The Church-Rosser property for \u03b2\u03b7-reduction in typed \u03bb-calculi. In LICS, pages 453\u2013460. IEEE, 1992.","DOI":"10.1109\/LICS.1992.185556"},{"key":"11_CR10","unstructured":"N. Ghani. Eta expansions in 179-01. To appear in proceedings CSL'96, Utrecht."},{"key":"11_CR11","unstructured":"N. Ghani. Adjoint Rewriting. PhD thesis, University of Edinburgh, Department of Computer Science, 1995."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"N. Ghani. \u03b2\u03b7-equality for coproducts. In Typed \u03bb -calculus and Applications, number 902 in Lecture Notes in Computer Science, pages 171\u2013185. Springer Verlag, 1995.","DOI":"10.1007\/BFb0014052"},{"key":"11_CR13","unstructured":"G. Huet. R\u00e9solution d'\u00e9quations dans des langages d'ordre 1,2, ..., \u03b5. Th\u00e8se d'Etat, Universit\u00e9 de Paris VII, 1976."},{"issue":"2","key":"11_CR14","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, Volume 5(2), April 1995, pages 135\u2013154. CUP 1995.","journal-title":"Journal of Functional Programming"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and H\u00e9l\u00e8ne Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15(4), November 1986.","DOI":"10.1137\/0215084"},{"key":"11_CR16","unstructured":"G. E. Mints. Teorija categorii i teoria dokazatelstv.i. Aktualnye problemy logiki i metodologii nauky, pages 252\u2013278, 1979."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"D. Prawitz. Ideas and results in proof theory. In J.E. Fenstad, editor, Proc. 2nd Scandinavian Logic Symposium, pages 235\u2013307. North Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62688-3_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:31:42Z","timestamp":1742599902000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62688-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540626886","9783540684381"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-62688-3_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}