{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:13:01Z","timestamp":1761610381945,"version":"build-2065373602"},"reference-count":26,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4958,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2000]]},"DOI":"10.1016\/s1571-0661(05)80127-6","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T08:37:08Z","timestamp":1117010228000},"page":"24-42","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":6,"special_numbering":"C","title":["The simply typed rewriting calculus"],"prefix":"10.1016","volume":"36","author":[{"given":"Horatiu","family":"Cirstea","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80127-6_BIBAC96","series-title":"Springer Verlag","article-title":"A Theory of Objects","author":"Abadi","year":"1996"},{"key":"10.1016\/S1571-0661(05)80127-6_BKK98","doi-asserted-by":"crossref","unstructured":"P. Borovansk\u00fd, C. Kirchner, H. Kirchner, P. E. Moreau, and C. Ringeissen. An overview of elan. In C. Kirchner and H. Kirchner, editors, Proceedings of the second International Workshop on Rewriting Logic and Applications, volume 15, Pont-\u00e0-Mousson (France), September 1998. Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/S1571-0661(05)82552-6"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBBOR98","series-title":"Th\u00e8se de Doctorat d'Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9 - Nancy 1, France","article-title":"Le contr\u01d2le de la r\u00e9\u00e9criture: \u00e9tude et implantation d'un formalisme de strat\u00e9gies","author":"Borovansk\u00fd","year":"1998"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBCELM96","doi-asserted-by":"crossref","unstructured":"M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In J. Meseguer, editor, Proceedings of the first international workshop on rewriting logic, volume 4, Asilomar (California), September 1996. Electronic Notes in Theoretical Computer Science.","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBCIR00","unstructured":"H. Cirstea. Le Rho Calcul: Fondements et Applications, PhD thesis, Universi\u00e9 Henri Poincar\u00e9 - Nancy I, 2000. to appear."},{"key":"10.1016\/S1571-0661(05)80127-6_BIBCK99A","first-page":"95","article-title":"Combining higher-order and first-order computation using p-calculus: Towards a semantics of ELAN","volume":"0863802524","author":"Cirstea","year":"1999"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBCK99B","article-title":"An introduction to the rewriting calculus","author":"Cirstea","year":"1999","journal-title":"Research Report RR-3818, INRIA"},{"journal-title":"Matching power","year":"2000","author":"Cirstea","key":"10.1016\/S1571-0661(05)80127-6_BIBCKL00"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBDEU96","first-page":"1","article-title":"An Overview of ASF+SDF","author":"Deursen","year":"1996"},{"issue":"1\/2","key":"10.1016\/S1571-0661(05)80127-6_BIBDHK00","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/inco.1999.2837","article-title":"Higher-order unification via explicit substitutions","volume":"157","author":"Dowek","year":"2000","journal-title":"Information and Computation"},{"issue":"1","key":"10.1016\/S1571-0661(05)80127-6_BIBFHM94","first-page":"3","article-title":"A Lambda Calculus of Objects and Method Specialization","volume":"1","author":"Fisher","year":"1994","journal-title":"Nordic Journal of Computing"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBFN97","unstructured":"K. Futatsugi and A. Nakagawa. An overview of CAFE specification environment - an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In Proceedings of the 1st IEEE Int. Conference on Formal Engineering Methods, 1997."},{"key":"10.1016\/S1571-0661(05)80127-6_BIBGAN80","series-title":"Essays on Combinatory Logic, Lambda Calculus, and Formalism","article-title":"Proof of strong normalisation","author":"Gandy","year":"1980"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBGBT89","first-page":"137","article-title":"Polymorphic rewriting conserves algebraic strong normalization and confluence","author":"Gallier","year":"1989"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBGIR72","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionnelle et elimination des coupures de I'arithm\u00e9tique d'ordre sup\u00e9rieur, PhD thesis, Universit\u00e9 Paris VII, June 1972."},{"key":"10.1016\/S1571-0661(05)80127-6_BIBHIN97","series-title":"volume 42 of Cambridge Tracts in Theoretical Computer Science","article-title":"Basic Simple Type Theory","author":"Hindley","year":"1997"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBHS86","series-title":"Cambridge University","article-title":"Introduction to Combinators and Lambda-calculus","author":"Hindley","year":"1986"},{"year":"1976","series-title":"R\u00e9solution d'equations dans les langages d'ordre 1,2, \u2026,\u03c9.","author":"Huet","key":"10.1016\/S1571-0661(05)80127-6_BIBHUE76"},{"issue":"2","key":"10.1016\/S1571-0661(05)80127-6_BIBJO97","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/S0304-3975(96)00161-2","article-title":"Abstract data type systems","volume":"173","author":"Jouannaud","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBKKV93","unstructured":"C. Kirchner, H. Kirchner, and M. Vittek. Implementing computational systems with constraints. In P. Kanellakis, J.-L. Lassez, and V. Saraswat, editors, Proceedings of the first Workshop on Principles and Practice of Constraint Programming, Providence (R.I., USA), pages 166-175. Brown University, 1993."},{"key":"10.1016\/S1571-0661(05)80127-6_BIBMES92","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBMI184","doi-asserted-by":"crossref","unstructured":"R. Milner. A proposal for standard ML. In Proceedings ACM Conference on LISP and Functional Programming, 1984.","DOI":"10.1145\/800055.802035"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBOKA89","doi-asserted-by":"crossref","unstructured":"M. Okada. Strong normalizability for the combined system of the typed Lambda-calculus and an arbitrary convergent term rewrite system. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, Portland (Oregon), pages 357-363. ACM Press, July 1989. Report CRIN 89-R-220.","DOI":"10.1145\/74540.74582"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBPJ87","series-title":"Prentice Hall, Inc.","article-title":"The implementation of functional programming languages","author":"Peyton-Jones","year":"1987"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBTAI67","doi-asserted-by":"crossref","DOI":"10.2307\/2271658","article-title":"Intensional interpretation of functionals of finite type I","volume":"32","author":"Tait","year":"1967","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(05)80127-6_BIBVIS99","series-title":"Rewriting Techniques and Applications (RTA '99), volume 1631 of Lecture Notes in Computer Science","first-page":"30","article-title":"Strategic pattern matching","author":"Visser","year":"1999"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801276?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105801276?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:28Z","timestamp":1761610108000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105801276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"references-count":26,"alternative-id":["S1571066105801276"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80127-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The simply typed rewriting calculus","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(05)80127-6","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2000 Elsevier B.V.","name":"copyright","label":"Copyright"}]}}