{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:25Z","timestamp":1775873545344,"version":"3.50.1"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2015,9,16]],"date-time":"2015-09-16T00:00:00Z","timestamp":1442361600000},"content-version":"unspecified","delay-in-days":258,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this article, we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high-level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations.<\/jats:p>","DOI":"10.1017\/s0956796815000180","type":"journal-article","created":{"date-parts":[[2015,9,16]],"date-time":"2015-09-16T05:15:49Z","timestamp":1442380549000},"source":"Crossref","is-referenced-by-count":15,"title":["Calculating correct compilers"],"prefix":"10.1017","volume":"25","author":[{"given":"PATRICK","family":"BAHR","sequence":"first","affiliation":[]},{"given":"GRAHAM","family":"HUTTON","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,9,16]]},"reference":[{"key":"S0956796815000180_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813672"},{"key":"S0956796815000180_ref15","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"S0956796815000180_ref3","doi-asserted-by":"crossref","unstructured":"Ager M. S. , Biernacki D. , Danvy O. & Midtgaard J. (2003b) From Interpreter to Compiler and Virtual Machine: A Functional Derivation. Technical Report RS-03-14. BRICS, Department of Computer Science, Aarhus, Denmark: University of Aarhus.","DOI":"10.7146\/brics.v10i14.21784"},{"key":"S0956796815000180_ref16","unstructured":"McKinna J. & Wright J. (2006) A Type-Correct, Stack-Safe, Provably Correct Expression Compiler in Epigram. Unpublished manuscript."},{"key":"S0956796815000180_ref24","doi-asserted-by":"crossref","unstructured":"Wadler P. (1989) Theorems for free! In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture. New York, NY, USA: ACM Press.","DOI":"10.1145\/99370.99404"},{"key":"S0956796815000180_ref7","first-page":"229","article-title":"Implementation of exception handling, Part I","volume":"5","author":"Chase","year":"1994","journal-title":"J. C Lang. Transl."},{"key":"S0956796815000180_ref19","doi-asserted-by":"crossref","unstructured":"Sculthorpe N. , Farmer A. & Gill A. (2013) The HERMIT in the tree: Mechanizing program transformations in the GHC Core language. Implementation and Application of Functional Languages 2012, Lecture Notes in Computer Science, vol. 8241. New York, NY, USA: Springer.","DOI":"10.1007\/978-3-642-41582-1_6"},{"key":"S0956796815000180_ref17","unstructured":"Meijer E. (1992) Calculating Compilers. Ph.D. thesis, Katholieke Universiteit Nijmegen."},{"key":"S0956796815000180_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_12"},{"key":"S0956796815000180_ref2","doi-asserted-by":"crossref","unstructured":"Ager M. S. , Biernacki D. , Danvy O. & Midtgaard J. (2003a) A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. New York, NY, USA: ACM, pp. 8\u201319.","DOI":"10.1145\/888251.888254"},{"key":"S0956796815000180_ref20","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"S0956796815000180_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796815000180_ref1","doi-asserted-by":"crossref","unstructured":"Adams N. , Kranz D. , Kelsey R. , Rees J. , Hudak P. & Philbin J. (1986) ORBIT: An optimizing compiler for scheme. In Proceedings of the 1986 SIGPLAN Symposium on Compiler Construction. New York, NY, USA: ACM, pp. 219\u2013233.","DOI":"10.1145\/13310.13333"},{"key":"S0956796815000180_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357179"},{"key":"S0956796815000180_ref23","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020887011500"},{"key":"S0956796815000180_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"S0956796815000180_ref5","volume-title":"Program Construction: Calculating Implementations from Specifications","author":"Backhouse","year":"2003"},{"key":"S0956796815000180_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_14"},{"key":"S0956796815000180_ref8","first-page":"20","article-title":"Implementation of exception handling, Part II","volume":"6","author":"Chase","year":"1994","journal-title":"J. C Lang. Transl."},{"key":"S0956796815000180_ref9","unstructured":"Day L. E. & Hutton G. (2014) Compilation \u00e0 la Carte. In Proceedings of the 25th Symposium on Implementation and Application of Functional Languages. New York, NY, USA: ACM, pp. 13\u201324."},{"key":"S0956796815000180_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006363"},{"key":"S0956796815000180_ref14","unstructured":"Letouzey P. (2008) Extraction in Coq: An overview. Logic and Theory of Algorithms: 4th Conference on Computability in Europe, Lecture Notes in Computer Science, vol. 5028. Berlin, Germany: Springer-Verlag."},{"key":"S0956796815000180_ref18","doi-asserted-by":"crossref","unstructured":"Reynolds J. C. (1972) Definitional interpreters for higher-order programming languages. In Proceedings of the ACM Annual Conference. New York, NY, USA: ACM, pp. 717\u2013740.","DOI":"10.1145\/800194.805852"},{"key":"S0956796815000180_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90056-J"},{"key":"S0956796815000180_ref22","volume-title":"Rabbit: A Compiler for Scheme","author":"Steele","year":"1978"},{"key":"S0956796815000180_ref26","doi-asserted-by":"crossref","unstructured":"Wand M. (1982b) Semantics-directed machine architecture. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 234\u2013241.","DOI":"10.1145\/582153.582179"},{"key":"S0956796815000180_ref27","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages \u2013 An Introduction","author":"Winskel","year":"1993"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796815000180","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,21]],"date-time":"2022-05-21T22:19:48Z","timestamp":1653171588000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796815000180\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":27,"alternative-id":["S0956796815000180"],"URL":"https:\/\/doi.org\/10.1017\/s0956796815000180","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e14"}}