{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:04Z","timestamp":1725664444597},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592938"},{"type":"electronic","value":"9783540492337"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59293-8_223","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:12:32Z","timestamp":1330276352000},"page":"605-619","source":"Crossref","is-referenced-by-count":3,"title":["Mechanized inductive proof of properties of a simple code optimizer"],"prefix":"10.1007","author":[{"given":"Alfons","family":"Geser","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Leo Bachmair. Proof by consistency in equational theories. In 3rd Proc. IEEE Symp. Logic in Computer Science, pages 228\u2013233, July 1988.","key":"40_CR1","DOI":"10.1109\/LICS.1988.5122"},{"key":"40_CR2","volume-title":"Technical Report MPI-I-93-249","author":"L. Bachmair","year":"1993","unstructured":"Leo Bachmair and Harald Ganzinger. Rewrite techniques for transitive relations. Technical Report MPI-I-93-249, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, November 1993."},{"key":"40_CR3","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0167-6423(88)90064-0","volume":"11","author":"R. Berghammer","year":"1988","unstructured":"Rudolf Berghammer, Herbert Ehler, and Hans Zierer. Towards an algebraic specification of code generation. Science of Computer Programming, 11:45\u201363, 1988. Also as technical report TUM-I8707, June, 1987, Technische Universit\u00e4t M\u00fcnchen, Germany.","journal-title":"Science of Computer Programming"},{"unstructured":"Robert S. Boyer and J. Strother Moore. A computational logic handbook. Academic Press, 1988.","key":"40_CR4"},{"doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, chapter 6, pages 243\u2013320. Elsevier, 1990.","key":"40_CR5","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"40_CR6","volume-title":"Technical Report MIP-9401","author":"U. Fraus","year":"1994","unstructured":"Ulrich Fraus. Inductive theorem proving for algebraic specifications \u2014 TIP system user's manual. Technical Report MIP-9401, Universit\u00e4t Passau, Germany, February 1994."},{"key":"40_CR7","volume-title":"The Unified Computation Laboratory \u2014 Unifying Frameworks, Theories and Tools","author":"U. Fraus","year":"1992","unstructured":"Ulrich Fraus and Heinrich Hu\u00dfmann. Term induction proofs by a generalization of narrowing. In C. Rattray and R. G. Clark, editors, The Unified Computation Laboratory \u2014 Unifying Frameworks, Theories and Tools, Oxford, UK, 1992. Clarendon Press."},{"issue":"3","key":"40_CR8","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0747-7171(89)80069-0","volume":"8","author":"L. Fribourg","year":"1989","unstructured":"Laurent Fribourg. A strong restriction of the inductive completion procedure. J. Symbolic Computation, 8(3):253\u2013276, September 1989.","journal-title":"J. Symbolic Computation"},{"doi-asserted-by":"crossref","unstructured":"Alfons Geser. A specification of the intel 8085 microprocessor \u2014 a case study. In [18], pages 347\u2013402, 1987.","key":"40_CR9","DOI":"10.1007\/BFb0015045"},{"key":"40_CR10","volume-title":"Systems for Computer-Aided Specification, Development, and Verification. Technical report 9416","author":"A. Geser","year":"1994","unstructured":"Alfons Geser. Mechanized inductive proof of properties of a simple code optimizer. In Bettina Buth and Rudolf Berghammer, editors, Systems for Computer-Aided Specification, Development, and Verification. Technical report 9416, Universit\u00e4t Kiel, Germany, October 1994."},{"doi-asserted-by":"crossref","unstructured":"Alfons Geser and Heinrich Hu\u00dfmann. Experiences with the RAP system \u2014 a specification interpreter combining term rewriting and resolution. In Bernard Robinet and Reinhard Wilhelm, editors, 2nd European Symposium on Programming, pages 339\u2013350. Springer LNCS 213, March 1986.","key":"40_CR11","DOI":"10.1007\/3-540-16442-1_26"},{"key":"40_CR12","first-page":"180","volume-title":"Proving inductive theorems based on term rewriting systems","author":"D. Hofbauer","year":"1988","unstructured":"Dieter Hofbauer and Ralf-Detlef Kutsche. Proving inductive theorems based on term rewriting systems. In Proc. Algebraic and Logic Programing, pages 180\u2013190, Gau\u00dfig, Germany, 1988. Springer LNCS 343."},{"unstructured":"Heinrich Hu\u00dfmann. A case study towards algebraic specification of code generation. In Maurice Nivat, C. Rattray, Teodor Rus, and Giuseppe Scollo, editors, Algebraic Methodology and Software Technology 91, Workshops in Computing, pages 254\u2013263. Springer, 1992.","key":"40_CR13"},{"doi-asserted-by":"crossref","unstructured":"Heinrich Hu\u00dfmann and Christian Rank. Specification and prototyping of a compiler for a small applicative language. In [18], pages 403\u2013418, 1987.","key":"40_CR14","DOI":"10.1007\/BFb0015046"},{"doi-asserted-by":"crossref","unstructured":"J. Levy and J. Agust\u00ed. Bi-rewriting, a term rewriting technique for monotonic order relations. In Claude Kirchner, editor, Int. Conf. Rewriting Techniques and Applications, pages 17\u201331. Springer LNCS 690, 1993.","key":"40_CR15","DOI":"10.1007\/3-540-56868-9"},{"unstructured":"Teodor Rus. Algebraic alternative for compiler construction. In IMA Conf. on the Unified Computation Laboratory, pages 144\u2013152, Stirling, Scotland, 1990.","key":"40_CR16"},{"key":"40_CR17","volume-title":"Formal Models and Semantics, Handbook of Theoretical Computer Science, Vol. B","author":"M. Wirsing","year":"1990","unstructured":"Martin Wirsing. Algebraic specification. In J. van Leeuwen, editor, Formal Models and Semantics, Handbook of Theoretical Computer Science, Vol. B. Elsevier \u2014 The MIT Press, 1990."},{"unstructured":"Martin Wirsing and Jan A. Bergstra. Algebraic methods: Theory, Tools, and Applications. Springer LNCS 394, June 1987.","key":"40_CR18"},{"issue":"4","key":"40_CR19","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"W. D. Young","year":"1989","unstructured":"William D. Young. A mechanically verified code generator. J. Automated Reasoning, 5(4):493\u2013518, 1989.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '95: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59293-8_223.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:26:39Z","timestamp":1605648399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59293-8_223"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592938","9783540492337"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-59293-8_223","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}