{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:40:15Z","timestamp":1742589615106,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540102502"},{"type":"electronic","value":"9783540383390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1980]]},"DOI":"10.1007\/3-540-10250-7_22","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:07:03Z","timestamp":1330189623000},"page":"165-188","source":"Crossref","is-referenced-by-count":5,"title":["More on advice on structuring compilers and proving them correct"],"prefix":"10.1007","author":[{"given":"James W.","family":"Thatcher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric G.","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jesse B.","family":"Wright","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,25]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/321992.321997","volume":"24","author":"J. A. Goguen","year":"1975","unstructured":"(1975) (JAG, JWT, EGW, JBW) \"Initial algebra semantics and continuous algebras,\" IBM Research Report RC-5701. November 1975. JACM 24 (1977) pp. 68\u201395.","journal-title":"JACM"},{"key":"5_CR2","unstructured":"(1976) (JWT, EGW, JBW) J. W. Thatcher, E. G. Wagner, and J. B. Wright \"Specification of abstract data types using conditional axioms,\" IBM Research Report RC-6214, September 1976."},{"key":"5_CR3","unstructured":"(1976a) (JAG, JWT, EGW) J. A. Goguen J. W. Thatcher E. G. Wagner \"An initial algebra approach to the specification, correctness, and implementation of abstract data types,\" IBM Research Report RC-6487, October 1976. To appear, Current Trends in Programming Methodology, IV: Data Structuring (R. Yeh, Ed.), pp. 80\u2013149, Prentice Hall, New Jersey."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"(1976b) (EGW, JBW, JAG, JWT) E. G. Wagner, J. B. Wright, J. A. Goguen, and J. W. Thatcher \"Some fundamentals of order algebraic semantics.\" Lecture Notes in Computer Science 45 (Mathematical Foundations of Computer Science 1976), Springer-Verlag, pp. 153\u2013168; IBM Research Report RC 6020, May 1976.","DOI":"10.1007\/3-540-07854-1_169"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"(1976c) \"Rational algebraic theories and fixed-point solutions,\" Proceedings 17th IEEE Symposium on Foundations of Computing, Houston, Texas, October, 1976, pp. 147\u2013158.","DOI":"10.1109\/SFCS.1976.24"},{"key":"5_CR6","unstructured":"(1977) (EGW, JWT, JBW) E. G. Wagner, J. W. Thatcher, J. B. Wright \"Free continuous theories,\" IBM Research Report RC 6906, December, 1977. Accepted for publication, Fundamenta Informaticae."},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1016\/S0019-9958(68)90374-4","volume":"12","author":"M. A. Arbib","year":"1968","unstructured":"Arbib, M.A. and Giveon, Y. (1968) \"Algebra automata I: Parallel programming as a prolegomena to the categorical approach,\" Information and Control 12 (1968) 331\u2013345.","journal-title":"Information and Control"},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/S0021-9800(70)80014-X","volume":"8","author":"G. Birkhoff","year":"1970","unstructured":"Birkhoff, G. and Lipson, J.D. (1970) \"Heterogeneous algebras,\" J. Combinatorial Theory 8 (1970) 115\u2013133.","journal-title":"J. Combinatorial Theory"},{"key":"5_CR9","unstructured":"Burstall, R.M. and Landin, P.J. (1969) \"Programs and their proofs: an algebraic approach,\" Machine Intelligence 4, 1969."},{"key":"5_CR10","unstructured":"Elgot, C.C. (1973) \"Monadic computation and iterative algebraic theories,\" IBM Research Report RC 4564, October 1973. Proceedings, Logic Colloquium 1973, North Holland (1975) 175\u2013230."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"(1977) Elgot, C.C. \"Some geometrical categories associated with flow chart schemes,\" IBM Research Report RC 6534, May 1977. Proceedings, Conference on Fundamentals of Computation Theory, Poznan-Kornik, Poland, 1977.","DOI":"10.1007\/3-540-08442-8_92"},{"key":"5_CR12","unstructured":"Elgot, C.C. and Shepherdson, J.C. (1977) \"A semantically meaningful characterization of reducible flow chart schemes,\" IBM Research Report RC 6656, July, 1977."},{"key":"5_CR13","unstructured":"Fiebrich, Rolf-Dieter (1978) \"Generation of correct compiler parts from formal language descriptions,\" LRZ-Bericht Nr. 7802\/1, Institut f\u00fcr Informatik der Ludwig-Maximilians-Universit\u00e4t, M\u00fcchen, 1978."},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Gaudel, M.C. (1980) \"Specification of compilers as abstract data type representations,\" draft manuscript, IRIA, Paris France. Presented, Workshop on Semantics Directed Compiler Generation, Aarhus, Denmark, January 1980.","DOI":"10.1007\/3-540-10250-7_21"},{"key":"5_CR15","unstructured":"(1980a) Gaudel, M.C. Thesis, March, 1980."},{"key":"5_CR16","first-page":"370","volume":"10","author":"G. Gremano","year":"1975","unstructured":"Gremano, G. and Maggiolo-Schettini, A. (1975) \"Proving a compiler correct: A simple approach,\" JCSS 10 (1975) 370\u2013383.","journal-title":"JCSS"},{"key":"5_CR17","unstructured":"Guttag, J. V. (1975) \"The specification and application to programming of abstract data types,\" Univ. of Toronto, Computer Systems Research Group, Technical Report CSRG-59, September, 1975."},{"key":"5_CR18","doi-asserted-by":"crossref","first-page":"869","DOI":"10.1073\/pnas.50.5.869","volume":"50","author":"F. W. Lawvere","year":"1963","unstructured":"Lawvere, F.W. (1963) \"Functorial semantics of algebraic theories,\" Proceedings, Nat'l Acad. Sci. 50 (1963) 869\u2013872.","journal-title":"Nat'l Acad. Sci."},{"key":"5_CR19","series-title":"Proceedings of Symposia in Applied Mathematics","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1090\/psapm\/019\/0242403","volume-title":"\"Correctness of a compiler for arithmetic expressions,\" Mathematical Aspects of Computer Science","author":"J. McCarthy","year":"1967","unstructured":"McCarthy, J. and Painter, J. (1967) \"Correctness of a compiler for arithmetic expressions,\" Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, Vol. 19 (J.T. Schwartz, Ed.) American Math. Soc., Providence R.I. (1967) 33\u201341."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Milner, R. (1972) \"Implementation and application of Scott's logic for computable functions,\" Proceedings, ACM Conference on Proving Assertions about Programs, Las Cruces, New Mexico, January, 1972, pp. 1\u20136.","DOI":"10.1145\/800235.807067"},{"key":"5_CR21","series-title":"Mathematical Centre Tracts","first-page":"3","volume-title":"Program semantics and mechanized proof","author":"R. Milner","year":"1976","unstructured":"(1976) \"Program semantics and mechanized proof,\" Mathematical Centre Tracts 82 (K.R. Apt and J.W. de Bakker (Eds.), Mathematisch Centrum, Amsterdam, 1976, pp. 3\u201344."},{"key":"5_CR22","unstructured":"Milner, R. and Weyrauch, R (1972) \"Proving compiler correctness in a mechanized logic,\" Machine Intelligence 7 (B. Meltzer and D. Michie, Eds.), Edinburgh University Press (1972) 51\u201372."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Morris, F. L. (1972) \"Correctness of translations of programming languages,\" Stanford Computer Science Memo CS 72\u2013303 (1972).","DOI":"10.21236\/ADA954771"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"(1973) Morris, F. L. \"Advice on structuring compilers and proving them correct,\" Proceedings, ACM Symposium on Principles of Programming Languages, Boston (1973) 144\u2013152.","DOI":"10.1145\/512927.512941"},{"key":"5_CR25","unstructured":"Mosses, P. (1977) \"Making denotational semantics less concrete,\" manuscript, Aarhus University, August, 1977."},{"key":"5_CR26","unstructured":"(1978) Mosses, P. \"Modular denotational semantics,\" Draft paper, 1978-11-11, Department of Computer Science, Institute of Mathematics, Aarhus University, 1978."},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"(1979) Mosses, P. \"A constructive approach to compiler correctness,\" draft manuscript, Department of Computer Science, Aarhus University, November 1979. Presented, Workshop on Semantics Directed Compiler Generation, Aarhus, January, 1980.","DOI":"10.1007\/3-540-10250-7_23"},{"key":"5_CR28","unstructured":"Schmeck, Hartmut (1975) \"Korrektheit von \u00dcbersetzungen,\" Bericht Nr. 3\/75 des Institut f\u00fcr Infromatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t Kiel, 1975."},{"key":"5_CR29","unstructured":"Scott, D. and Strachey, C. (1971) \"Toward a mathematical semantics for computer languages,\" Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group, 1971."},{"key":"5_CR30","unstructured":"Zilles, S. N. (1974) \"Algebraic specification of data types,\" Computation Structures Group Memo 119, MIT, Cambridge, Mass. (1974) 28\u201352."}],"container-title":["Lecture Notes in Computer Science","Semantics-Directed Compiler Generation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-10250-7_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:11:00Z","timestamp":1742587860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-10250-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980]]},"ISBN":["9783540102502","9783540383390"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-10250-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1980]]}}}