{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:10:59Z","timestamp":1773097859348,"version":"3.50.1"},"reference-count":18,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":6247,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1991,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The \u03bb\u03c3-calculus is a refinement of the \u03bb-calculus where substitutions are manipulated explicitly. The \u03bb\u03c3-calculus provides a setting for studying the theory of substitutions, with pleasant mathematical properties. It is also a useful bridge between the classical \u03bb-calculus and concrete implementations.<\/jats:p>","DOI":"10.1017\/s0956796800000186","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T16:14:25Z","timestamp":1226074465000},"page":"375-416","source":"Crossref","is-referenced-by-count":320,"title":["Explicit substitutions"],"prefix":"10.1017","volume":"1","author":[{"given":"M.","family":"Abadi","sequence":"first","affiliation":[]},{"given":"L.","family":"Cardelli","sequence":"additional","affiliation":[]},{"given":"P.-L.","family":"Curien","sequence":"additional","affiliation":[]},{"given":"J.-J.","family":"L\u00e9vy","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000186_ref009","unstructured":"Comptes Rendus de l'Acad\u00e9mie des Sciences de Paris, t. 312, S\u00e9rie I, pp. 471\u201376."},{"key":"S0956796800000186_ref008","unstructured":"Curien P.-L. and R\u00edos A. 1991. Un R\u00e9sultat de Compl\u00e9tude pour les Substitutions Explicites."},{"key":"S0956796800000186_ref010","volume-title":"Combinatory Logic","volume":"1","author":"Curry","year":"1958"},{"key":"S0956796800000186_ref014","unstructured":"Hardin T. and L\u00e9vy J.-J. 1989. A confluent calculus of substitutions. In France\u2013Japan Artificial Intelligence and Computer Science Symposium, Izu, Japan, December."},{"key":"S0956796800000186_ref007","doi-asserted-by":"crossref","unstructured":"Curien P.-L. , Hardin T. and R\u00edos A. 1991 b. Normalisation forte des substitutions (draft).","DOI":"10.1007\/3-540-55808-X_19"},{"key":"S0956796800000186_ref006","unstructured":"Curien P.-L. , Hardin T. and L\u00e9vy J.-J. 1991 a. Confluence properties of weak and strong calculi of explicit substitutions (draft)."},{"key":"S0956796800000186_ref004","volume-title":"Categorical Combinators, Sequential Algorithms and Functional Programming","author":"Curien","year":"1986"},{"key":"S0956796800000186_ref016","volume-title":"Combinatory Reduction Systems","author":"Klop","year":"1980"},{"key":"S0956796800000186_ref005","unstructured":"Curien P.-L. 1988. The \u03bb\u03c0-calculi: an Abstract Framework for Closures, unpublished (preliminary version printed as LIENS report)."},{"key":"S0956796800000186_ref002","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796800000186_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"S0956796800000186_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90035-6"},{"key":"S0956796800000186_ref003","unstructured":"Cardelli L. 1989. Typeful Programming, SRC Report No. 45. Digital Equipment Corporation."},{"key":"S0956796800000186_ref011","unstructured":"Field J. 1990. On laziness and optimality in lambda interpreters: tools for specification and analysis. In 17th Annual ACM Symposium on Principles of Programming Languages, San Francisco, USA, january, pp. 1\u201315."},{"key":"S0956796800000186_ref001","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1985"},{"key":"S0956796800000186_ref017","unstructured":"Martin-L\u00f6f P. 1984. Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padova in 1980. Bibliopolis."},{"key":"S0956796800000186_ref018","unstructured":"Wadsworth C. P. 1971. Semantics and Pragmatics of the Lambda Calculus, Dissertation, Oxford University."},{"key":"S0956796800000186_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90105-9"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000186","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T15:30:14Z","timestamp":1738510214000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000186\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,10]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1991,10]]}},"alternative-id":["S0956796800000186"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000186","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,10]]}}}