{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:45:06Z","timestamp":1758055506475,"version":"3.44.0"},"reference-count":27,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"unspecified","delay-in-days":257,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>This paper explores a principled approach to calculating abstract machines and associated compilers, starting from an intrinsically typed interpreter. After deriving a compiler for a simple expression language in some detail, the first steps of this calculation are repeated to derive an optimizing evaluator for the simply typed lambda calculus.<\/jats:p>","DOI":"10.1017\/s0956796825100087","type":"journal-article","created":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T08:41:59Z","timestamp":1757925719000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Towards type-directed compiler calculation"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0295-7944","authenticated-orcid":false,"given":"WOUTER","family":"SWIERSTRA","sequence":"first","affiliation":[{"name":"Utrecht University"}]}],"member":"56","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"S0956796825100087_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"S0956796825100087_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357179"},{"key":"S0956796825100087_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S0956796825100087_ref21","unstructured":"Norell, U. (2007) Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology."},{"key":"S0956796825100087_ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3677999.3678283"},{"key":"S0956796825100087_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3591241"},{"key":"S0956796825100087_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"S0956796825100087_ref24","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.76.10"},{"key":"S0956796825100087_ref11","unstructured":"Elliott, C. (2020) Calculating Compilers Categorically. Unpublished draft."},{"key":"S0956796825100087_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328474"},{"key":"S0956796825100087_ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3473587"},{"key":"S0956796825100087_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"S0956796825100087_ref26","first-page":"344","volume-title":"European Symposium on Programming","author":"Wadler","year":"1988"},{"key":"S0956796825100087_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"S0956796825100087_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000180"},{"key":"S0956796825100087_ref7","first-page":"52","volume-title":"Symposium on Implementation and Application of Functional Languages","author":"Danvy","year":"2004"},{"key":"S0956796825100087_ref10","article-title":"Refocusing in reduction semantics","volume":"11","author":"Danvy","year":"2004","journal-title":"BRICS Rep. Ser"},{"key":"S0956796825100087_ref14","article-title":"Continuation-passing style, defunctionalization, accumulations, and associativity","volume":"6","author":"Gibbons","year":"2022","journal-title":"Art Sci. Eng. Program."},{"key":"S0956796825100087_ref18","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.275.6"},{"key":"S0956796825100087_ref19","unstructured":"McKinna, J. & Wright, J. (2006) A Type-Correct, Stack-Safe, Provably Correct Expression Compiler. Accepted for publication in the Journal of Functional Programming.Please provide complete information for reference McKinna & Wright (2006)."},{"key":"S0956796825100087_ref6","doi-asserted-by":"crossref","unstructured":"Bahr, P. & Hutton, G. (2022) Monadic compiler calculation. Proc. ACM Program. Lang. 6(ICFP), 93:1\u201393:29.","DOI":"10.1145\/3547624"},{"key":"S0956796825100087_ref20","unstructured":"Meijer, E. (1992) Calculating Compilers. PhD thesis, Radboud Universiteit Nijmegen."},{"key":"S0956796825100087_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000209"},{"key":"S0956796825100087_ref3","unstructured":"Augustsson, L. & Carlsson, M. (1999) An exercise in dependent types: A well-typed interpreter. In Workshop on Dependent Types in Programming, Gothenburg."},{"key":"S0956796825100087_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3240719.3241787"},{"key":"S0956796825100087_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_3"},{"key":"S0956796825100087_ref13","unstructured":"Gibbons, J. (2002) Calculating functional programs. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction: International Summer School and Workshop Oxford, UK, April 10\u201314, 2000 Revised Lectures, pp. 151\u2013203. Springer."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796825100087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T08:42:01Z","timestamp":1757925721000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796825100087\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":27,"alternative-id":["S0956796825100087"],"URL":"https:\/\/doi.org\/10.1017\/s0956796825100087","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e20"}}