{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T11:51:24Z","timestamp":1648813884586},"reference-count":27,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3674,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Computer and System Sciences"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1016\/s0022-0000(03)00048-5","type":"journal-article","created":{"date-parts":[[2003,5,12]],"date-time":"2003-05-12T21:09:12Z","timestamp":1052773752000},"page":"127-173","source":"Crossref","is-referenced-by-count":1,"title":["Proof theory of higher-order equations: conservativity, normal forms and term rewriting"],"prefix":"10.1016","volume":"67","author":[{"given":"K.","family":"Meinke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0022-0000(03)00048-5_BIB1","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1017\/S0305004100013463","article-title":"On the structure of abstract algebras","volume":"31","author":"Birkhoff","year":"1935","journal-title":"Proc. Cambridge Philos. Soc."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB3","series-title":"Isomorphisms of Types: From Lambda Calculus to Information Retrieval and Language Design","author":"Di Cosmo","year":"1995"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB4","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.-P. Jouannaud, Rewrite systems, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B, North-Holland, Amsterdam, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB5","series-title":"Topology","author":"Dugundji","year":"1966"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB6","series-title":"Fundamentals of Algebraic Specification 1","author":"Ehrig","year":"1985"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB7","series-title":"Handbook of Mathematical Logic","article-title":"Theories of finite type related to mathematical practice","author":"Feferman","year":"1977"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB8","article-title":"Proofs and Types","volume":"Vol. 7","author":"Girard","year":"1989"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB9","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/947886.947887","article-title":"Completeness of many-sorted equational logic","volume":"17","author":"Goguen","year":"1982","journal-title":"Assoc. Comput. Mach. SIGPLAN Notices"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB10","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"2","author":"Henkin","year":"1950","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB11","series-title":"Introduction to Combinators and Lambda Calculus","author":"Hindley","year":"1986"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB12","series-title":"General Topology","author":"Kelley","year":"1955"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB13","unstructured":"J.W. Klop, Term rewriting systems, in: S. Abramsky, D. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, Vol. II, Oxford University Press, Oxford, 1993, pp. 1\u2013111."},{"issue":"1","key":"10.1016\/S0022-0000(03)00048-5_BIB14","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1006\/inco.1996.0007","article-title":"On the power of higher-order algebraic specifications","volume":"124","author":"Kosiuczenko","year":"1995","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB15","series-title":"Introduction to Higher Order Categorical Logic","author":"Lambek","year":"1986"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB16","series-title":"Canonical Forms in Finitely Presented Algebras","author":"Le Chenadec","year":"1986"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB17","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1016\/0304-3975(92)90310-C","article-title":"Universal algebra in higher types","volume":"100","author":"Meinke","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB18","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/BF01178510","article-title":"A recursive second-order initial algebra specification of primitive recursion","volume":"31","author":"Meinke","year":"1994","journal-title":"Acta Inform."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB19","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1006\/jcss.1997.1489","article-title":"A completeness theorem for the expressive power of higher-order algebraic specifications","volume":"54","author":"Meinke","year":"1997","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB20","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/PL00013322","article-title":"Correctness of dataflow and systolic algorithms using algebras of streams","volume":"38","author":"Meinke","year":"2001","journal-title":"Acta Inform."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB21","series-title":"Handbook of Logic in Computer Science","first-page":"189","article-title":"Universal algebra","author":"Meinke","year":"1992"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB22","series-title":"Recent Trends in Data Type Specification","first-page":"154","article-title":"Algebraic specifications of reachable higher-order algebras","volume":"Vol. 332","author":"M\u00f6ller","year":"1988"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB23","article-title":"Recursion on the Countable Functionals","volume":"Vol. 811","author":"Normann","year":"1980"},{"key":"10.1016\/S0022-0000(03)00048-5_BIB24","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","article-title":"Mathematical logic as based on the theory of types","volume":"30","author":"Russel","year":"1908","journal-title":"Amer. J. Math."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB25","unstructured":"L.J. Steggles, Extensions of higher-order algebra: fundamental theory and case studies, Ph.D. Thesis, Dept. of Computer Science, University of Wales, Swansea, 1995."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB26","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1016\/0022-0000(87)90023-7","article-title":"On observational equivalence and algebraic specification","volume":"34","author":"Sanella","year":"1987","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/S0022-0000(03)00048-5_BIB27","unstructured":"W. Taylor, Equational logic, Houston J. Math. (1979) 1\u201383, also in: G. Gr\u00e4tzer, Universal Algebra, 2nd Edition, Springer, Berlin, 1979."}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000003000485?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000003000485?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T09:53:54Z","timestamp":1553162034000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0022000003000485"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["S0022000003000485"],"URL":"https:\/\/doi.org\/10.1016\/s0022-0000(03)00048-5","relation":{},"ISSN":["0022-0000"],"issn-type":[{"value":"0022-0000","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}