{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:16Z","timestamp":1776891436058,"version":"3.51.2"},"reference-count":3,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,9,20]],"date-time":"2017-09-20T00:00:00Z","timestamp":1505865600000},"content-version":"unspecified","delay-in-days":262,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Fifty years ago, John McCarthy and James Painter (1967) published the first paper on compiler verification, in which they showed how to formally prove the correctness of a compiler that translates arithmetic expressions into code for a register-based machine. In this article, we revisit this example in a modern context, and show how such a compiler can now be calculated directly from a specification of its correctness using simple equational reasoning techniques.<\/jats:p>","DOI":"10.1017\/s0956796817000120","type":"journal-article","created":{"date-parts":[[2017,9,20]],"date-time":"2017-09-20T01:28:52Z","timestamp":1505870932000},"source":"Crossref","is-referenced-by-count":3,"title":["Compiling a 50-year journey"],"prefix":"10.46298","volume":"27","author":[{"given":"GRAHAM","family":"HUTTON","sequence":"first","affiliation":[]},{"given":"PATRICK","family":"BAHR","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2017,9,20]]},"reference":[{"key":"S0956796817000120_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000180"},{"key":"S0956796817000120_ref3","doi-asserted-by":"crossref","unstructured":"McCarthy J. & Painter J. (1967) Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, vol. 19. American Mathematical Society.","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"S0956796817000120_ref2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781316784099","volume-title":"Programming in Haskell","author":"Hutton","year":"2016"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796817000120","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:51Z","timestamp":1776889191000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796817000120\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":3,"alternative-id":["S0956796817000120"],"URL":"https:\/\/doi.org\/10.1017\/s0956796817000120","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e20"}}