{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:15Z","timestamp":1725664995485},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617563"},{"type":"electronic","value":"9783540706540"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61756-6_98","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:20:44Z","timestamp":1330294844000},"page":"378-392","source":"Crossref","is-referenced-by-count":2,"title":["Generalized \u03b2-reduction and explicit substitutions"],"prefix":"10.1007","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Alejandro","family":"R\u00edos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"issue":"4","key":"26_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit Substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call by need lambda calculus. Conf. Rec. 22nd Ann. ACM Symp. Princ. Program. Lang. ACM, 1995.","DOI":"10.1145\/199448.199507"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"H. Barendregt. \u03bb-calculi with types. Handbook of Logic in Computer Science, II, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Z. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. \u03bb\u03bd, a calculus of explicit substitutions which preserves strong normalisation. Personal communication, 1995.","DOI":"10.1017\/S0956796800001945"},{"key":"26_CR5","unstructured":"R. Bloo. Preservation of Strong Normalisation for Explicit Substitution. Technical Report 95-08, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1995."},{"issue":"2","key":"26_CR6","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1006\/inco.1996.0041","volume":"126","author":"R. Bloo","year":"1996","unstructured":"R. Bloo, F. Kamareddine, and R. Nederpelt. The Barendregt Cube with Definitions and Generalised Reduction. Information and Computation, 126 (2):123\u2013143, 1996.","journal-title":"Information and Computation"},{"key":"26_CR7","unstructured":"R. Constable et al. Implementing Mathematics with the NUPRL Development System. Prentice-Hall, 1986."},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986. Revised edition: Birkh\u00e4user (1993).","DOI":"10.1007\/978-1-4612-0317-9"},{"key":"26_CR9","volume-title":"Technical Report RR 1617","author":"P.-L. Curien","year":"1992","unstructured":"P.-L. Curien, T. Hardin, and J.-J. L\u00e9vy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report RR 1617, INRIA, Rocquencourt, 1992."},{"key":"26_CR10","unstructured":"N. G. de Bruijn. A namefree lambda calculus with facilities for internal definition of expressions and segments. Technical Report TH-Report 78-WSK-03, Department of Mathematics, Eindhoven University of Technology, 1978."},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"P. de Groote. The conservation theorem revisited. Int'l Conf. Typed Lambda Calculi and Applications LNCS, 664, 1993.","DOI":"10.1007\/BFb0037105"},{"key":"26_CR12","unstructured":"G. Dowek et al. The coq proof assistant version 5.6, users guide. Technical Report 134, INRIA, 1991."},{"key":"26_CR13","unstructured":"F. Kamareddine. A reduction relation for which postponement of k-contractions, conservation and preservation of strong normalisation hold. Technical report, Glasgow University, 1996."},{"key":"26_CR14","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(95)00101-8","volume":"155","author":"F. Kamareddine","year":"1996","unstructured":"F. Kamareddine and R. Nederpelt. A useful \u03bb-notation. Theoretical Computer Science, 155:85\u2013109, 1996.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"26_CR15","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1142\/S0129054193000146","volume":"4","author":"F. Kamareddine","year":"1993","unstructured":"F. Kamareddine and R. P. Nederpelt. On stepwise explicit substitution. International Journal of Foundations of Computer Science, 4(3):197\u2013240, 1993.","journal-title":"International Journal of Foundations of Computer Science"},{"issue":"4","key":"26_CR16","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1017\/S0956796800001507","volume":"5","author":"F. Kamareddine","year":"1995","unstructured":"F. Kamareddine and R. P. Nederpelt. Generalising reduction in the \u03bb-calculus. Journal of Functional Programming, 5(4):637\u2013651, 1995.","journal-title":"Journal of Functional Programming"},{"key":"26_CR17","first-page":"45","volume":"982","author":"F. Kamareddine","year":"1995","unstructured":"F. Kamareddine and A. R\u00edos. A \u03bb-calculus \u00e0 la de Bruijn with explicit substitutions. Proceedings of PLILP'95. LNCS, 982:45\u201362, 1995.","journal-title":"LNCS"},{"key":"26_CR18","unstructured":"F. Kamareddine and A. R\u00edos. The \u03bbs-calculus: its typed and its extended versions. Technical report, Department of Computing Science, University of Glasgow, 1995."},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and A. R\u00edos. Extending a \u03bb-calculus with Explicit Substitution which preserves Strong Normalisation into a Confluent Calculus on Open Terms. Journal of Functional Programming, 1996. To appear.","DOI":"10.1017\/S0956796897002785"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and A. R\u00edos. Generalised \u03b2-reduction and explicit substitutions. Technical Report TR-1996-21, Department of Computing Science, University of Glasgow, 1996.","DOI":"10.1007\/3-540-61756-6_98"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"M. Karr. Delayability in proofs of strong normalizability in the typed \u03bb-calculus. Mathematical Foundations of Computer Software, LNCS, 185, 1985.","DOI":"10.1007\/3-540-15198-2_13"},{"issue":"2","key":"26_CR22","first-page":"368","volume":"41","author":"A.J. Kfoury","year":"1994","unstructured":"A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. An analysis of ML typability. ACM, 41(2):368\u2013398, 1994.","journal-title":"ACM"},{"key":"26_CR23","unstructured":"A.J. Kfoury and J.B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second order \u03bb-calculus. Proc. 1994 ACM Conf. LISP Funct. Program., 1994."},{"key":"26_CR24","unstructured":"A.J. Kfoury and J.B. Wells. Addendum to new notions of reduction and nonsemantic proofs of \u03b2-strong normalisation in typed \u03bb-calculi. Technical report, Boston University, 1995."},{"key":"26_CR25","unstructured":"A.J. Kfoury and J.B. Wells. New notions of reductions and non-semantic proofs of \u03b2-strong normalisation in typed \u03bb-calculi. LICS, 1995."},{"key":"26_CR26","doi-asserted-by":"crossref","unstructured":"Z. Khasidashvili. The longest perpetual reductions in orthogonal expression reduction systems. Proc. of the 3rd International Conference on Logical Foundations of Computer Science, Logic at St Petersburg, 813, 1994.","DOI":"10.1007\/3-540-58140-5_20"},{"key":"26_CR27","unstructured":"J. W. Klop. Combinatory Reduction Systems. Mathematical Center Tracts, 27, 1980."},{"key":"26_CR28","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e8s. Typed \u03bb-calculi with explicit substitutions may not terminate in Proceedings of TLCA'95. LNCS, 902, 1995.","DOI":"10.1007\/BFb0014062"},{"key":"26_CR29","volume-title":"Technical Report 2762","author":"C. A. Mu\u00f1oz Hurtado","year":"1995","unstructured":"C. A. Mu\u00f1oz Hurtado. Confluence and preservation of strong normalisation in an explicit substitutions calculus. Technical Report 2762, INRIA, Rocquencourt, December 1995."},{"key":"26_CR30","volume-title":"Selected papers on Automath","author":"R. P. Nederpelt","year":"1994","unstructured":"R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Selected papers on Automath. North-Holland, Amsterdam, 1994."},{"key":"26_CR31","unstructured":"S.L. Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987."},{"key":"26_CR32","unstructured":"L. Regnier. Lambda calcul et r\u00e9seaux. PhD thesis, Paris 7, 1992."},{"key":"26_CR33","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/0304-3975(94)90012-4","volume":"126","author":"L. Regnier","year":"1994","unstructured":"L. Regnier. Une \u00e9quivalence sur les lambda termes. Theoretical Computer Science, 126:281\u2013292, 1994.","journal-title":"Theoretical Computer Science"},{"key":"26_CR34","unstructured":"A. R\u00edos. Contribution \u00e0 l'\u00e9tude des \u03bb-calculs avec substitutions explicites. PhD thesis, Universit\u00e9 de Paris 7, 1993."},{"key":"26_CR35","doi-asserted-by":"crossref","unstructured":"A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. Proc. 1992 ACM Conf. LISP Funct. Program., pages 288\u2013298, 1992.","DOI":"10.1145\/141471.141563"},{"key":"26_CR36","unstructured":"M. S\u00f8rensen. Strong normalisation from weak normalisation in typed \u03bb-calculi. Submitted."},{"key":"26_CR37","unstructured":"D. Vidal. Nouvelles notions de r\u00e9duction en lambda calcul. PhD thesis, Universit\u00e9 de Nancy 1, 1989."},{"key":"26_CR38","unstructured":"H. Xi. On weak and strong normalisations. Technical Report 96-187, Carnegie Mellon University, 1996."}],"container-title":["Lecture Notes in Computer Science","Programming Languages: Implementations, Logics, and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61756-6_98.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:46:10Z","timestamp":1713635170000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61756-6_98"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617563","9783540706540"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/3-540-61756-6_98","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}