{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:13:35Z","timestamp":1648512815392},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,6,1]],"date-time":"2006-06-01T00:00:00Z","timestamp":1149120000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2006,6]]},"DOI":"10.1007\/s00236-006-0013-0","type":"journal-article","created":{"date-parts":[[2006,6,2]],"date-time":"2006-06-02T12:44:12Z","timestamp":1149252252000},"page":"1-43","source":"Crossref","is-referenced-by-count":0,"title":["Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information"],"prefix":"10.1007","volume":"43","author":[{"given":"Klaus","family":"Indermark","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Noll","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,3]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0304-3975(76)90031-1","volume":"2","author":"J. Bakker","year":"1976","unstructured":"Bakker J. (1976). Least fixed points revisited. Theoret. Comput. Sci. 2:155\u2013181","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Brus, T., van Eekelen, M., van Leer, M., Plasmeijer, R.: Clean: a language for functional graph rewriting. In: Proceedings of the ACM Symposium on Functional Programming Languages and Computer Architecture (FPCA\u00a0\u201987), Lecture Notes in Computer Science, vol. 274, pp. 364\u2013384. Springer, Berlin Heidelberg New York (1987)","DOI":"10.1007\/3-540-18317-5_20"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Cadiou, J.: Recursive definitions of partial functions and their computation. Ph.D. Thesis, Stanford University (1972)","DOI":"10.1145\/800235.807072"},{"key":"13_CR4","doi-asserted-by":"crossref","first-page":"253","DOI":"10.3233\/FI-1997-313404","volume":"31","author":"O. Chitil","year":"1997","unstructured":"Chitil O. (1997). The \u03c2\u2013semantics: a comprehensive semantics for functional programs. Fundam Inform 31:253\u2013294","journal-title":"Fundam Inform"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Proceedings of the Rewriting Techniques and Applications (RTA\u00a0\u201903), Lecture Notes in Computer Science, vol. 2706, pp. 258\u2013263. Springer, Berlin Heidelberg New York (2003)","DOI":"10.1007\/3-540-44881-0_7"},{"key":"13_CR6","unstructured":"Diaconescu, R., Futatsugi, K., Ishisone, M., Sawada, T., Nakagawa, A.: An overview of CafeOBJ. In: Proceedings of the Second International Workshop on Rewriting Logic and its Applications (WRLA\u00a0\u201998), Electronic Notes in Theoretical Computer Science, vol. 15, pp. 75\u201388. Elsevier (1998).http:\/\/www.elsevier.nl\/locate\/entcs\/volume15.html"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Goguen, J., Kirchner, C., Kirchner, H., M\u00e9grelis, A., Meseguer, J.: An introduction to OBJ3. In: Proceedings of the Workshop on Conditional Term Rewriting Systems, Lecture Notes in Computer Science, vol. 308, pp. 258\u2013263. Springer, Berlin Heidelberg New York (1988)","DOI":"10.1007\/3-540-19242-5_22"},{"issue":"1","key":"13_CR8","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/321992.321997","volume":"24","author":"J. Goguen","year":"1977","unstructured":"Goguen J., Thatcher J., Wagner E., Wright J. (1977). Initial algebra semantics and continuous algebras. J. ACM 24(1):68\u201395","journal-title":"J. ACM"},{"key":"13_CR9","volume-title":"Theory of Program Structures. No. 36 in Lecture Notes in Computer Science","author":"S. Greibach","year":"1975","unstructured":"Greibach S. (1975). Theory of Program Structures. No. 36 in Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York"},{"key":"13_CR10","volume-title":"Functional Programming. International Series in Computer Science","author":"P. Henderson","year":"1980","unstructured":"Henderson P. (1980). Functional Programming. International Series in Computer Science. Prentice-Hall, Englewood Cliffs"},{"key":"13_CR11","unstructured":"Indermark, K., Noll, T.: Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information. No. 2004\u201308 in Aachener Informatik\u2013Bericht. RWTH Aachen University (2004). Available online at http:\/\/sunsite.informatik.rwth-aachen.de\/Publications\/AIB\/2004\/"},{"key":"13_CR12","unstructured":"Kleene, S.: Introduction to Metamathematics. North-Holland, (1952)"},{"issue":"4","key":"13_CR13","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P. Landin","year":"1964","unstructured":"Landin P. (1964). The mechanical evaluation of expressions. Comput. J. 6(4):308\u2013320","journal-title":"Comput. J."},{"issue":"7","key":"13_CR14","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/361454.361460","volume":"15","author":"Z. Manna","year":"1972","unstructured":"Manna Z., Vuillemin J. (1972). Fixpoint approach to the theory of computation. Commun. ACM 15(7):528\u2013536","journal-title":"Commun. ACM"},{"key":"13_CR15","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J. McCarthy","year":"1960","unstructured":"McCarthy J. (1960). Recursive functions of symbolic expressions and their computation by machine, part I. Commun ACM 3:184\u2013195","journal-title":"Commun ACM"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. In: Proceedings Symposium in Applied Mathematics, Mathematical Aspects of Computer Science 19, 33\u201341 (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Noll, T.: On the first-order equivalence of call-by-name and call-by-value. In: Proceedings of the Colloquium on Trees in Algebra and Programming (CAAP\u00a0\u201994), no. 787 in Lecture Notes in Computer Science, pp. 246\u2013260. Springer, Berlin Heidelberg New York (1994)","DOI":"10.1007\/BFb0017486"},{"key":"13_CR18","unstructured":"Noll, T.: Klassen applikativer Programmschemata und ihre Berechnungsst\u00e4rke in German. Ph.D. Thesis, RWTH Aachen University (1995)."},{"issue":"2","key":"13_CR19","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/366959.366968","volume":"3","author":"K. Samelson","year":"1960","unstructured":"Samelson K., Bauer F. (1960). Sequential formula translation. Comm. ACM 3(2):76\u201383","journal-title":"Comm. ACM"},{"key":"13_CR20","unstructured":"Schl\u00f6r, R.: Korrektheit der \u00dcbersetzung rekursiver Funktionsdefinitionen in Stackcode in German. Master\u2019s Thesis, RWTH Aachen University (1987)."},{"key":"13_CR21","unstructured":"Scott, D.: Outline of a mathematical theory of computation. In: Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems, vol. 3, pp. 169\u2013176 (1970)"},{"key":"13_CR22","unstructured":"Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. In: Proceedings of the Symposium on Computers and Automata, pp. 19\u201346. Wiley, New York (1972)"},{"key":"13_CR23","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"Tarski A. (1955). A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5:285\u2013309","journal-title":"Pac. J. Math."},{"key":"13_CR24","volume-title":"Haskell","author":"S. Thompson","year":"1999","unstructured":"Thompson S. (1999). Haskell, 2nd edn. Addison-Wesley, Reading","edition":"2"},{"issue":"2","key":"13_CR25","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1145\/234528.234738","volume":"28","author":"P. Wadler","year":"1996","unstructured":"Wadler P. (1996). Lazy versus strict. ACM Comput. Surv. 28(2):318\u2013320","journal-title":"ACM Comput. Surv."},{"key":"13_CR26","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel G. (1993). The Formal Semantics of Programming Languages. MIT Press, Cambridge"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0013-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-006-0013-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-006-0013-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,15]],"date-time":"2020-04-15T06:29:06Z","timestamp":1586932146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-006-0013-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,6]]}},"alternative-id":["13"],"URL":"https:\/\/doi.org\/10.1007\/s00236-006-0013-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6]]}}}