{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T14:52:22Z","timestamp":1649083942659},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T00:00:00Z","timestamp":1172275200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2007,4,4]]},"DOI":"10.1007\/s10990-007-9004-2","type":"journal-article","created":{"date-parts":[[2007,2,24]],"date-time":"2007-02-24T03:22:59Z","timestamp":1172287379000},"page":"37-72","source":"Crossref","is-referenced-by-count":1,"title":["A \u03c1-calculus of explicit constraint application"],"prefix":"10.1007","volume":"20","author":[{"given":"Horatiu","family":"Cirstea","sequence":"first","affiliation":[]},{"given":"Germain","family":"Faure","sequence":"additional","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,2,24]]},"reference":[{"issue":"4","key":"9004_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. J. Func. Progr. 1(4), 375\u2013416 (1991)","journal-title":"J. Func. Progr."},{"key":"9004_CR2","volume-title":"The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics. 2nd edn. Elsevier Science Publishers B.V. (North-Holland), Amsterdam (1984)","edition":"2nd edn"},{"key":"9004_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure patterns type systems. In: Principles of Programming Languages\u2014POPL2003, New Orleans, USA. ACM (2003)","DOI":"10.1145\/604131.604152"},{"issue":"1\u20133","key":"9004_CR4","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/S0019-9958(82)90458-2","volume":"55","author":"K. Berkling","year":"1982","unstructured":"Berkling, K., Fehr, E.: A consistent extension of the lambda-calculus as a base for functional programming languages. Inform. Contr. 55(1\u20133), 89\u2013101 (1982)","journal-title":"Inform. Contr."},{"key":"9004_CR5","doi-asserted-by":"crossref","unstructured":"Bloo, R., Rose, K.H.: Combinatory reduction systems with explicit substitution that preserve strong nomalisation. In: Proceedings of the Fifth International Conference on Rewriting Techniques and Application (RTA \u201996), pp. 169\u2013183 (1996)","DOI":"10.1007\/3-540-61464-8_51"},{"key":"9004_CR6","doi-asserted-by":"crossref","unstructured":"Borovansk\u00fd, P.: Controlling rewriting: study and implementation of a strategy formalism. Elect. Notes Theor. Comp. Sci. 15 (1998)","DOI":"10.1016\/S1571-0661(05)80018-0"},{"key":"9004_CR7","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner, H.: A functional view of rewriting and strategies for a semantics of ELAN. In: Sato, M., Toyama, Y. (eds.) The Third Fuji International Symposium on Functional and Logic Programming, pp. 143\u2013167. Kyoto (1998). World Scientific. Also report LORIA 98-R-165"},{"key":"9004_CR8","doi-asserted-by":"crossref","unstructured":"Borovansk\u00fd, P., Kirchner, C., Kirchner H., Moreau, P.-E., Ringeissen, C.: An overview of ELAN. In: Proceedings of Workshop on Rewriting Techniques and Application\u2014WRLA\u20191998, vol. 15. Electronic Notes in Theoretical Computer Science (1998) Report LORIA 98-R-316","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"9004_CR9","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1002\/(SICI)1097-024X(200003)30:3<259::AID-SPE298>3.0.CO;2-Y","volume":"30","author":"M. van den Brand","year":"2000","unstructured":"van den Brand, M., de Jong, H., Klint, P., Olivier, P.: Efficient annotated terms. Softw. Prac. Exp. 30, 259\u2013291 (2000)","journal-title":"Softw. Prac. Exp."},{"key":"9004_CR10","unstructured":"Chailloux, E., Manoury. P., Pagano, B.: D\u00e9veloppement d\u2019applications avec Objective CAML. O\u2019REILLY (2000)"},{"key":"9004_CR11","unstructured":"Cirstea, H.: Calcul de r\u00e9\u00e9criture: fondements et applications. PhD thesis, Universit\u00e9 Henri Poincar\u00e9\u2014Nancy I (2000)"},{"key":"9004_CR12","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Faure, G., Kirchner, C.: A rho-calculus of explicit constraint application. In: Workshop on Rewriting Logic and Applications, Barcelona (Spain) (2004). Electronic Notes in Theoretical Computer Science","DOI":"10.1016\/j.entcs.2004.06.029"},{"issue":"3","key":"9004_CR13","first-page":"427","volume":"9","author":"H. Cirstea","year":"2001","unstructured":"Cirstea, H., Kirchner, C.: The rewriting calculus\u2014Part I and II. Logic J. Interest Group in Pure and Appl. Logics 9(3), 427\u2013498 (2001)","journal-title":"Logic J. Interest Group in Pure and Appl. Logics"},{"key":"9004_CR14","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C., Liquori, L.: Matching Power. In: Proceedings of Rewriting Techniques and Applications RTA\u20192001, http:\/\/www.springer.de\/comp\/lncs\/index.html Lecture Notes in Computer Science, Utrecht (The Netherlands). Springer-Verlag (2001)","DOI":"10.1007\/3-540-45127-7_8"},{"key":"9004_CR15","unstructured":"Cirstea, H., Kirchner, C., Liquori, L.: Rewriting calculus with(out) types. In: Fabio Gadducci, Ugo Montanari (eds.) Proceedings of the Fourth Workshop on Rewriting Logic and Applications, Pisa (Italy) (2002). Electronic Notes in Theoretical Computer Science"},{"key":"9004_CR16","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C., Liquori, L., Wack, B.: Rewrite strategies in the rewriting calculus. In: Proceedings of the Third International Workshop on Reduction Strategies in Rewriting and Programming, Valencia, Spain (2003). Electronic Notes in Theoretical Computer Science","DOI":"10.1016\/S1571-0661(05)82613-1"},{"key":"9004_CR17","doi-asserted-by":"crossref","unstructured":"Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Jos\u00e9 Meseguer (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol. 4. Asilomar (California) (1996). Electronic Notes in Theoretical Computer Science","DOI":"10.1016\/S1571-0661(04)00034-9"},{"issue":"2","key":"9004_CR18","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. J. ACM (JACM) 43(2), 362\u2013397 (1996)","journal-title":"J. ACM (JACM)"},{"key":"9004_CR19","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1017\/S0960129500003224","volume":"11","author":"R. David","year":"2001","unstructured":"David, R., Guillaume, B.: A \u03bb-calculus with explicit weakening and explicit substitution. Math. Struct. Comp. Sci. 11, 169\u2013206 (2001)","journal-title":"Math. Struct. Comp. Sci."},{"key":"9004_CR20","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/S1385-7258(78)80025-0","volume":"40","author":"N. de Bruijn","year":"1978","unstructured":"de Bruijn, N.: Lambda calculus with namefree formulas involving symbols that represent reference transforming mappings. Indagationes Mathematicae 40, 348\u2013356 (1978)","journal-title":"Indagationes Mathematicae"},{"key":"9004_CR21","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: A lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae 34, 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"issue":"1\/2","key":"9004_CR22","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Higher order unification via explicit substitutions. Inform. Comp. 157(1\/2), 183\u2013235 (2000)","journal-title":"Inform. Comp."},{"issue":"5","key":"9004_CR23","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1093\/comjnl\/38.5.381","volume":"38","author":"S. Eker","year":"1995","unstructured":"Eker, S.: Associative-commutative matching via bipartite graph matching. Comp. J. 38(5), 381\u2013399 (1995)","journal-title":"Comp. J."},{"key":"9004_CR24","doi-asserted-by":"crossref","unstructured":"Faure, G., Kirchner, C.: Exceptions in the rewriting calculus. In: Proceedings of Rewriting Techniques and Applications\u2014RTA\u20192002, vol. 2378 of LNCS, pp. 66\u201382, Copenhagen, Springer-Verlag (2002)","DOI":"10.1007\/3-540-45610-4_6"},{"key":"9004_CR25","doi-asserted-by":"crossref","unstructured":"Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanized Logic of Computation, vol. 78 of Lecture Notes in Computer Science. Springer-Verlag, New York (NY, USA) (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9004_CR26","doi-asserted-by":"crossref","unstructured":"Hendriks, D., van Oostrom, V.: The \u03bb calculus. In: Proceedings of Conference on Automated Deduction\u2014CADE\u20192003, vol. 2741 of Lecture Notes in Artificial Intelligence, pp. 136\u2013150 (2003)","DOI":"10.1007\/978-3-540-45085-6_11"},{"issue":"5","key":"9004_CR27","first-page":"T-1","volume":"27","author":"P. Hudak","year":"1992","unstructured":"Hudak, P., Fasel, J.H.: A gentle introduction to Haskell. ACM SIGPLAN Notices 27(5), T-1\u2013T-53 (1992)","journal-title":"ACM SIGPLAN Notices"},{"key":"9004_CR28","unstructured":"Huet, G.: Resolution d\u2019Equations dans les Languages d\u2019Ordre 1,2,...,\u03c9. These de Doctorat D\u2019Etat, Universite Paris VII (1976)"},{"issue":"4","key":"9004_CR29","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980)","journal-title":"J. ACM"},{"issue":"4","key":"9004_CR30","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comp. 15(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comp."},{"key":"9004_CR31","doi-asserted-by":"crossref","unstructured":"Kesner, D., Lengrand, S.: Extending the explicit substitution paradigm. In: Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA \u201905), LNCS 256 (2005)","DOI":"10.1007\/978-3-540-32033-3_30"},{"key":"9004_CR32","doi-asserted-by":"crossref","unstructured":"Kirchner, C., Kirchner, H.: Rewriting, solving, proving. A preliminary version of a book available at | www.loria.fr\/~ckirchne\/rsp.ps.gz | (1999)","DOI":"10.1007\/978-3-642-59851-7_9"},{"key":"9004_CR33","doi-asserted-by":"crossref","unstructured":"Kirchner, C., Kirchner, H.: Rule-based programming and proving : the ELAN experience outcomes. In: Ninth Asian Computing Science Conference\u2014ASIAN\u201904, Chiang Mai, Thailand (2004)","DOI":"10.1007\/978-3-540-30502-6_27"},{"key":"9004_CR34","doi-asserted-by":"crossref","unstructured":"Kirchner, C., Moreau, P.-E., Reilles, A.: Formal validation of pattern matching code. In: PPDP \u201905: Proceedings of the 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 187\u2013197, ACM Press, New York, NY, USA (2005)","DOI":"10.1145\/1069774.1069792"},{"key":"9004_CR35","unstructured":"Klop, J.W.: Combinatory Reduction Systems. Ph.D. thesis, Mathematisch Centrum, Amsterdam (1980)"},{"key":"9004_CR36","unstructured":"Leroy, X.: Compiling functional languages. Summer school on Semantics of programming languages (2002)"},{"key":"9004_CR37","doi-asserted-by":"crossref","unstructured":"Lescanne, P.: From \u03bb\u03c3 to \u03bbv a journey through calculi of explicit substitutions. In: Conference Record of POPL \u201994, pp. 60\u201369. ACM (1994)","DOI":"10.1145\/174675.174707"},{"issue":"2","key":"9004_CR38","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10817-004-6885-1","volume":"33","author":"C. Liang","year":"2004","unstructured":"Liang, C., Nadathur, G.: Choices in representation and reduction strategies for lambda terms in intensional contexts. J. Auto. Reasoning 33(2), 89\u2013132 (2004)","journal-title":"J. Auto. Reasoning"},{"key":"9004_CR39","doi-asserted-by":"crossref","unstructured":"Liquori, L., Serpette, B.: irho: an imperative rewriting calculus. In: Proceedings of te International Conference on Principles and Practice of Declarative Programming (PPDP\u201904), pp. 167\u2013178 (2004)","DOI":"10.1145\/1013963.1013983"},{"key":"9004_CR40","doi-asserted-by":"crossref","unstructured":"Moreau, P.-E., Ringeissen, C., Vittek, M.: A Pattern Matching Compiler for Multiple Target Languages. In: Hedin G. (ed.) 12th Conference on Compiler Construction, Warsaw (Poland), vol. 2622 of LNCS, pp. 61\u201376. Springer-Verlag (2003)","DOI":"10.1007\/3-540-36579-6_5"},{"key":"9004_CR41","unstructured":"Mu\u00f1oz, C.: Un calcul de substitutions pour la repr\u00e9sentation de preuves partielles en th\u00e9orie de types. Th\u00e9se de doctorat, Universit\u00e9 Paris 7 (1997). English version available as INRIA research report RR-3309"},{"key":"9004_CR42","doi-asserted-by":"crossref","unstructured":"Nadathur, G.: The suspension notation for lambda terms and its use in metalanguage implementations. In: Ninth Workshop on Logic, Language, Information and Computation (WoLLIC\u201902) Electronic Notes in Theoretical Computer Science, vol. 67 (2002)","DOI":"10.1016\/S1571-0661(04)80539-5"},{"issue":"3\u20134","key":"9004_CR43","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1023\/A:1021975117537","volume":"29","author":"Q.-H. Nguyen","year":"2002","unstructured":"Nguyen, Q.-H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. J. Auto. Reasoning 29(3\u20134), 309\u2013336 (2002)","journal-title":"J. Auto. Reasoning"},{"key":"9004_CR44","doi-asserted-by":"crossref","unstructured":"Ohlebusch, E.: Church-rosser theorems for abstract reduction modulo an equivalence relation. In: Proceedings of Rewriting Techniques and Applications (RTA-98), vol. 1379 of LNCS, pp. 17\u201331. Springer (1998)","DOI":"10.1007\/BFb0052358"},{"key":"9004_CR45","doi-asserted-by":"crossref","unstructured":"Pagano, B.: X.R.S: Explicit reduction systems\u2014A first-order calculus for higher-order calculi. In: Proceedings of the International Conference on Automated Deduction (CADE \u201998), pp. 72\u201387 (1998)","DOI":"10.1007\/BFb0054249"},{"key":"9004_CR46","unstructured":"Rose, K.H.: Operational Reduction Models for Functional Programming Languages. Ph.D. Thesis, DIKU, University of Copenhagen, Denmark (1996)"},{"issue":"2","key":"9004_CR47","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1093\/logcom\/exi010","volume":"15","author":"F.-R. Sinot","year":"2005","unstructured":"Sinot, F.-R.: Director strings revisited: A generic approach to the efficient representation of free variables in higher-order rewriting. J. Log. Comput. 15(2), 201\u2013218 (2005)","journal-title":"J. Log. Comput."},{"key":"9004_CR48","doi-asserted-by":"crossref","unstructured":"Stehr, M.-O.: CINNI\u2014A generic calculus of explicit substitutions and its application to lambda-, varsigma- and pi-calculi. Elect. Notes Theor. Comp. Sci. 36 (2000)","DOI":"10.1016\/S1571-0661(05)80125-2"},{"key":"9004_CR49","unstructured":"Stump, A., Deivanayagam, A., Kathol, S., Lingelbach, D., Schobel, D.: Rogue decision procedures. In: 1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning\u2014PDPAR (2003)"},{"key":"9004_CR50","unstructured":"Wack, B.: Aspects logique du calcul de r\u00e9\u00e9criture. Ph.D. Thesis, Universit\u00e9 Henri Poincar\u00e9\u2014Nancy I (2005)"},{"issue":"1","key":"9004_CR51","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1137\/0219005","volume":"19","author":"H. Yokouchi","year":"1990","unstructured":"Yokouchi, H., Hikita, T.: A rewriting system for categorical combinators with multiple arguments. SIAM J. Comput. 19(1), 78\u201397 (1990)","journal-title":"SIAM J. Comput."}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9004-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9004-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9004-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:29:41Z","timestamp":1559352581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9004-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2,24]]},"references-count":51,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,4,4]]}},"alternative-id":["9004"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9004-2","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2,24]]}}}