{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T14:25:49Z","timestamp":1672237549780},"reference-count":24,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1975,6,1]],"date-time":"1975-06-01T00:00:00Z","timestamp":170812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":13926,"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":[[1975,6]]},"DOI":"10.1016\/s0022-0000(75)80007-9","type":"journal-article","created":{"date-parts":[[2010,11,10]],"date-time":"2010-11-10T04:46:40Z","timestamp":1289364400000},"page":"370-383","source":"Crossref","is-referenced-by-count":10,"title":["Proving a compiler correct: A simple approach"],"prefix":"10.1016","volume":"10","author":[{"given":"G.","family":"Germano","sequence":"first","affiliation":[]},{"given":"A.","family":"Maggiolo-Schettini","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0022-0000(75)80007-9_bib1","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1016\/S0022-0000(69)80016-4","article-title":"Towards a theory of semantics and compilers for programming languages","volume":"3","author":"Blum","year":"1969","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0022-0000(75)80007-9_bib2","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/362929.362947","article-title":"GO TO statements considered harmful","volume":"11","author":"Dijkstra","year":"1968","journal-title":"Comm. ACM."},{"key":"10.1016\/S0022-0000(75)80007-9_bib3","series-title":"Recursiveness","author":"Eilenberg","year":"1970"},{"key":"10.1016\/S0022-0000(75)80007-9_bib4","first-page":"426","article-title":"Eliminability of concluding formulas in Markov's normal algorithms","volume":"18","author":"Germano","year":"1971","journal-title":"Notices Amer. Math. Soc."},{"key":"10.1016\/S0022-0000(75)80007-9_bib5","first-page":"660","article-title":"Eliminability of concluding formulas in Markov's normal algorithms II","volume":"18","author":"Germano","year":"1971","journal-title":"Notices Amer. Math. Soc."},{"key":"10.1016\/S0022-0000(75)80007-9_bib6","series-title":"IVth International Congress for Logic, Methodology and Philosophy of Science, Centre of Information and Documentation in Social and Political Sciences","article-title":"Markov's normal algorithms without concluding formulas: an application","author":"Germano","year":"1971"},{"key":"10.1016\/S0022-0000(75)80007-9_bib7","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/BF02575518","article-title":"Equivalence of partial recursivity and computability by algorithms without concluding formulas","volume":"8","author":"Germano","year":"1971","journal-title":"Calcolo"},{"key":"10.1016\/S0022-0000(75)80007-9_bib8","first-page":"332","article-title":"A Characterization of partial recursive functions via sequence functions","volume":"19","author":"Germano","year":"1972","journal-title":"Notices Amer. Math. Soc."},{"key":"10.1016\/S0022-0000(75)80007-9_bib9","series-title":"Seminaires IRIA: Th\u00e9orie des Algorithmes, des Languages et de la Programmation","first-page":"33","article-title":"A new theory of calculability","author":"Germano","year":"1972"},{"key":"10.1016\/S0022-0000(75)80007-9_bib10","first-page":"1325","article-title":"Quelques caract\u00e9risations des fonctions r\u00e9cursives partielles","volume":"276","author":"Germano","year":"1973","journal-title":"C. R. Acad. Sci. Paris"},{"key":"10.1016\/S0022-0000(75)80007-9_bib11","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/BF01951941","article-title":"A flow diagram composition of Markov's normal algorithms without concluding formulas","volume":"13","author":"Germano","year":"1973","journal-title":"BIT"},{"key":"10.1016\/S0022-0000(75)80007-9_bib12","article-title":"Recursivity and models of programs","author":"Germano","year":"1973"},{"key":"10.1016\/S0022-0000(75)80007-9_bib13","article-title":"Sequence-to-sequence recursive functions: a systematic study","author":"Germano","year":"1974"},{"key":"10.1016\/S0022-0000(75)80007-9_bib14","article-title":"A language for Markov's algorithms composition","author":"Germano","year":"1973"},{"key":"10.1016\/S0022-0000(75)80007-9_bib15","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF01692511","article-title":"Semantics of context-free languages","volume":"2","author":"Knuth","year":"1968","journal-title":"Math. Systems Theory"},{"key":"10.1016\/S0022-0000(75)80007-9_bib16","series-title":"Proceedings of an ACM Conference on Proving Assertions about Programs","first-page":"121","article-title":"Correctness of a compiler for a LISP subset","author":"London","year":"1972"},{"key":"10.1016\/S0022-0000(75)80007-9_bib17","article-title":"Method and notation for the formal definition of programming languages","author":"Lucas","year":"1968"},{"key":"10.1016\/S0022-0000(75)80007-9_bib18","unstructured":"J. McCarthy, Towards a mathematical science of computation, in \u201dInformation Processing 62, Proceedings of IFIP Congress 62,\u201c pp. 21\u201328."},{"key":"10.1016\/S0022-0000(75)80007-9_bib19","doi-asserted-by":"crossref","unstructured":"J.McCarthy and J. Painter, Correctness of a compiler for arithmetic expressions, in \u201dMathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics,\u201c Vol. XIX, pp. 33\u201341.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"10.1016\/S0022-0000(75)80007-9_bib20","series-title":"Conference Record of an ACM Symposium on Principles of Programming Languages","first-page":"144","article-title":"Advice on structuring compilers and proving them correct","author":"Morris","year":"1973"},{"key":"10.1016\/S0022-0000(75)80007-9_bib21","article-title":"Towards a mathematical semantics for computer languages","author":"Scott","year":"1971"},{"key":"10.1016\/S0022-0000(75)80007-9_bib22","series-title":"Proceedings of an ACM Conference on Proving Assertions about Programs","first-page":"128","article-title":"Operational semantics of programming languages","author":"Wegner","year":"1972"},{"key":"10.1016\/S0022-0000(75)80007-9_bib23","unstructured":"W. A. Wulf, Programming without GO TO, in \u201cInformation Processing 71, Proceedingsof IFIP Congress 71,\u201d pp. 408\u2013413."},{"key":"10.1016\/S0022-0000(75)80007-9_bib24","series-title":"Proceedings of the ACM Annual Conference","first-page":"791","article-title":"A Case against GO TO","author":"Wulf","year":"1972"}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000075800079?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0022000075800079?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T01:11:10Z","timestamp":1559783470000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0022000075800079"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1975,6]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1975,6]]}},"alternative-id":["S0022000075800079"],"URL":"https:\/\/doi.org\/10.1016\/s0022-0000(75)80007-9","relation":{},"ISSN":["0022-0000"],"issn-type":[{"value":"0022-0000","type":"print"}],"subject":[],"published":{"date-parts":[[1975,6]]}}}