{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:19:26Z","timestamp":1725664766425},"publisher-location":"Berlin, Heidelberg","reference-count":38,"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_52","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:39:43Z","timestamp":1330292383000},"page":"184-199","source":"Crossref","is-referenced-by-count":9,"title":["Confluence properties of extensional and non-extensional \u03bb-calculi with explicit substitutions (extended abstract)"],"prefix":"10.1007","author":[{"given":"Delia","family":"Kesner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"1","key":"15_CR1","first-page":"375","volume":"4","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P-L. Curien, and J-J. L\u00e9vy. Explicit substitutions. JFP, 4(1):375\u2013416, 1991.","journal-title":"JFP"},{"key":"15_CR2","unstructured":"Y. Akama. On mints' reductions for ccc-calculus. In TLCA, LNCS 664, 1993."},{"key":"15_CR3","unstructured":"H. Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North Holland, 1984."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Z-E-A. Benaissa and D. Briaud and P. Lescanne and J. Rouyer-Degli. \u03bbv, a calculus of explicit substitutions which preserves strong normalisation. Available from http:\/\/www.loria.fr\/lescanne\/publications.html. 1995.","DOI":"10.1017\/S0956796800001945"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"D. Briaud. An explicit eta rewrite rule. In TLCA, LNCS 902, 1995.","DOI":"10.1007\/BFb0014047"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"P-L. Curien and R. Di Cosmo. A confluent reduction system for the \u03bb-calculus with surjective pairing and terminal object. In ICALP, LNCS 510, 1991.","DOI":"10.1007\/3-540-54233-7_142"},{"key":"15_CR7","unstructured":"P-L. Curien, T. Hardin, and J-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report 1617, INRIA Rocquencourt, 1992."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"P-L. Curien, T. Hardin, and A. R\u00edos. Strong normalisation of substitutions. In MFCS'92, LNCS 629, 1992.","DOI":"10.1007\/3-540-55808-X_19"},{"issue":"35","key":"15_CR9","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"5","author":"N. Bruijn de","year":"1972","unstructured":"N. de Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indag. Mat., 5(35):381\u2013392, 1972.","journal-title":"Indag. Mat."},{"key":"15_CR10","first-page":"384","volume":"40","author":"N. Bruijn de","year":"1978","unstructured":"N. de Bruijn. Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings. Indag. Mat., (40):384\u2013356, 1978.","journal-title":"Indag. Mat."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Roberto Di Cosmo and Delia Kesner. A confluent reduction for the extensional typed \u03bb-calculus with pairs, sums, recursion and terminal object. In ICALP, LNCS 700, 1993.","DOI":"10.1007\/3-540-56939-1_109"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Roberto Di Cosmo and Delia Kesner. Combining first order algebraic rewriting systems, recursion and extensional typed lambda calculi. In ICALP, LNCS 820, 1994.","DOI":"10.1007\/3-540-58201-0_90"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and D. Kesner. Rewriting with extensional polymorphic \u03bb-calculus. In CSL, 1995.","DOI":"10.1007\/3-540-61377-3_40"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"R. Di Cosmo and A. Pipemo. Expanding extensional polymorphism. In TLCA, LNCS 902, 1995.","DOI":"10.1007\/BFb0014050"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"D. Dougherty. Some lambda calculi with categorical sums and products. In RTA, LNCS 690, 1993.","DOI":"10.1007\/3-540-56868-9_12"},{"key":"15_CR16","unstructured":"Thomas Ehrhard. Une s\u00e9mantique cat\u00e9gorique des types d\u00e9pendants. Application au calcul des constructions. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1988."},{"key":"15_CR17","unstructured":"J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1990."},{"key":"15_CR18","unstructured":"T. Hardin. R\u00e9sultats de confluence pour les r\u00e8gles fortes de la logique combinatoire cat\u00e9gorique et liens avec les lambda-calculs. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1987."},{"key":"15_CR19","unstructured":"T. Hardin. \u03b7-reduction for explicit substitutions. In ALP'92, LNCS 632, 1992."},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/BF01188746","volume":"5","author":"T. Hardin","year":"1994","unstructured":"T. Hardin. Eta-conversion for the languages of explicit substitutions. AAECC, 5:317\u2013341, 1994.","journal-title":"AAECC"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"T. Hardin and A. Laville. Proof of termination of the rewriting system subst on c.c.l. TCS, 1986.","DOI":"10.1016\/0304-3975(86)90035-6"},{"key":"15_CR22","unstructured":"T. Hardin and J-J. L\u00e9vy. A confluent calculus of substitutions. In France-Japan Art. Int. and Comp. Sci. Symp., 1989."},{"key":"15_CR23","unstructured":"G. Huet. R\u00e9solution d'\u00e9quations dans les langages d'ordre 1,2,...,\u03c9. Th\u00e8se de doctorat d'\u00e9tat, Universit\u00e9 Paris VII, 1976."},{"issue":"2","key":"15_CR24","first-page":"135","volume":"5","author":"C. B. Jay","year":"1995","unstructured":"C. Barry Jay and N. Ghani. The virtues of eta-expansion. JFP, 5(2):135\u2013154, 1995.","journal-title":"JFP"},{"key":"15_CR25","doi-asserted-by":"crossref","unstructured":"D. Kesner. Confluence properties of extensional and non-extensional \u03bb-calculi with explicit substitutions, 1995. Available as ftp:\/\/ftp.lri.fr\/lri\/articles\/kesner\/explicit.ps.gz.","DOI":"10.1007\/3-540-61464-8_52"},{"key":"15_CR26","unstructured":"F. Kamareddine and A. R\u00edos. The confluence of the \u03bbs e -calculus via a generalized interpretation method, 1995. Draft."},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and A. R\u00edos. A \u03bb-calculus \u00e0 la de bruijn with explicit substitutions. In PULP, LNCS 982, 1995.","DOI":"10.1007\/BFb0026813"},{"key":"15_CR28","unstructured":"P. Lescanne. Personal Communication."},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"P. Lescanne. From \u03bb\u03c3 to \u03bbv, a journey through calculi of explicit substitutions. In POPL, pages 60\u201369. ACM, 1994.","DOI":"10.1145\/174675.174707"},{"key":"15_CR30","volume-title":"Technical Report","author":"P. Lescanne","year":"1994","unstructured":"P. Lescanne and J. Rouyer-Degli. The calculus of explicit substitutions \u03bbv. Technical Report, INRIA, Lorraine, 1994."},{"key":"15_CR31","volume-title":"PhD thesis","author":"C. March\u00e9","year":"1993","unstructured":"C. March\u00e9. R\u00e9\u00e9criture modulo une th\u00e9orie pr\u00e9sent\u00e9e par un syst\u00e8me convergent et d\u00e9cidabilit\u00e9 des probl\u00e8mes du mot dans certains classes de th\u00e9ories \u00e9quationnelles. PhD thesis, Universit\u00e9 Paris-Sud, Orsay, 1993."},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"P-A. Mellies. Typed \u03bb-calculi with explicit substitutions may not terminate. In TLCA, LNCS 902, 1995.","DOI":"10.1007\/BFb0014062"},{"key":"15_CR33","first-page":"83","volume":"68","author":"G. Mints","year":"1977","unstructured":"G. Mints. Closed categories and the theory of proofs. Zap. Nauch. Semin. Leningradskogo, 68:83\u2013114, 1977.","journal-title":"Zap. Nauch. Semin. Leningradskogo"},{"key":"15_CR34","unstructured":"G. Mints. Teorija categorii i teoria dokazatelstv.l. Aktualnye problemy logiki i metodologii nauky, pages 252\u2013278, 1979."},{"issue":"3","key":"15_CR35","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1305\/ndjfl\/1093883461","volume":"22","author":"G. Pottinger","year":"1981","unstructured":"G. Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Surjective Pairing. Notre Dame Jour. of Formal Logic, 22(3):264\u2013268, 1981.","journal-title":"Notre Dame Jour. of Formal Logic"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"D. Prawitz. Ideas and results in proof theory. Proceedings of the 2nd Scandinavian Logic Symposium, pages 235\u2013307, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"15_CR37","unstructured":"A. R\u00edos. Contribution \u00e0 l'\u00e9tude des \u03bb-calculus avec substitutions explicites. Th\u00e8se de doctorat, Universit\u00e9 de Paris VII, 1993."},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"V. van Oostrom and F. van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In LICS, 1994","DOI":"10.1007\/3-540-58140-5_35"}],"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_52.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:35:31Z","timestamp":1640946931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61464-8_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614647","9783540685968"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-61464-8_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}