{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T21:20:31Z","timestamp":1761945631720,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097790","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"134-153","source":"Crossref","is-referenced-by-count":3,"title":["A proof of weak termination of typed \u03bb\u03c3-calculi"],"prefix":"10.1007","author":[{"given":"Jean","family":"Goubault-Larrecq","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. In 17th PoPL, pages 31\u201346, 1990.","DOI":"10.1145\/96709.96712"},{"key":"8_CR2","unstructured":"D. Briaud. Higher-order unification as a typed narrowing. Technical Report 96-R-112, CRIN, 1996."},{"key":"8_CR3","unstructured":"R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract). In 12th LICS, 1997."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions (extended abstract). In 10th LICS, pages 366\u2013374, 1995.","DOI":"10.1109\/LICS.1995.523271"},{"key":"8_CR5","unstructured":"J. H. Gallier. On Girard's \u201ccandidats de r\u00e9ductibilit\u00e9\u201d. In P. Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Series, pages 123\u2013203. Academic Press, 1990."},{"key":"8_CR6","unstructured":"T. Hardin and J.-J. L\u00e9vy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, 1989."},{"key":"8_CR7","unstructured":"J.-L. Krivine. Lambda-calcul, types et mod\u00e8les. Masson, 1992."},{"key":"8_CR8","unstructured":"P. Lescanne. \u03c4 does not terminate. Working group of the PRC Math-Info \u201cM\u00e9langes de syst\u00e8mes de r\u00e9\u00e9criture alg\u00e9brique et de syst\u00e8mes logiques\u201d, 1996."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"P. Lescanne and J. Rouyer-Degli. From \u03bb\u03c3 to \u03bb\u03c1: a journey through calculi of explicit substitutions. In 21st PoPL, 1994.","DOI":"10.1145\/174675.174707"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed lambda-calculi with explicit substitutions may not terminate. In CONFER workshop, 1994.","DOI":"10.1007\/BFb0014062"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed lambda-calculi with explicit substitutions may not terminate. In 2nd TLCA, pages 328\u2013334. Springer Verlag LNCS 902, 1995.","DOI":"10.1007\/BFb0014062"},{"key":"8_CR12","unstructured":"C. A. Mu\u00f1oz Hurtado. Confluence and preservation of strong normalization in an explicit substitutions calculus. In 11th LICS, 1996."},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"C. A. Mu\u00f1oz Hurtado. Dependent types with explicit substitutions: A meta-theoretical development. In TYPES'96, 1997. This volume.","DOI":"10.1007\/BFb0097798"},{"key":"8_CR14","unstructured":"C. A. Mu\u00f1oz Hurtado. Meta-theoretical properties of \u03bb\u03c6: A left-linear variant of \u03bb\u03c3. Technical Report RR-3107, Inria, 1997."},{"key":"8_CR15","unstructured":"A. R\u00edos. Contributions \u00e0 l'\u00e9tude des lambda-calculus avec substitutions explicites. PhD thesis, \u00c9cole Normale Sup\u00e9rieure, 1993."},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","unstructured":"H. Zantema. Termination of term rewriting: Interpretation and type elimination. J. Symbolic Computation, 17:23\u201350, 1994.","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097790","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T04:24:59Z","timestamp":1736655899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097790"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0097790","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}