{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T21:06:46Z","timestamp":1770239206218,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/Y010744\/1"],"award-info":[{"award-number":["EP\/Y010744\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,15]]},"abstract":"<jats:p>Bahr and Hutton recently developed an approach to compiler calculation that allows a wide range of compilers to be derived from specifications of their correctness. However, a limitation of the approach is that it results in compilers that produce tree-structured code. By contrast, realistic compilers produce code that is essentially graph-structured, where the edges in the graph represent jumps that transfer the flow of control to other locations in the code. In this article, we show how their approach can naturally be adapted to calculate compilers that produce graph-structured code, without changing the underlying calculational methodology, by using a higher-order abstract syntax representation of graphs.<\/jats:p>","DOI":"10.1145\/3674638","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"370-394","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1600-8261","authenticated-orcid":false,"given":"Patrick","family":"Bahr","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Copenhagen, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9584-5150","authenticated-orcid":false,"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, Nottingham, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"crossref","unstructured":"Mads Sig Ager Dariusz Biernacki Olivier Danvy and Jan Midtgaard. 2003. From Interpreter to Compiler and Virtual Machine: A Functional Derivation. Technical Report RS-03-14. Department of Computer Science University of Aarhus.","DOI":"10.7146\/brics.v10i14.21784"},{"key":"e_1_3_1_3_1","doi-asserted-by":"crossref","unstructured":"Robert Atkey. 2009. Syntax for Free: Representing Syntax with Binding Using Parametricity. In Typed Lambda Calculi and Applications. Lecture Notes in Computer Science Vol. 5608.","DOI":"10.1007\/978-3-642-02273-9_5"},{"key":"e_1_3_1_4_1","volume-title":"Program Construction: Calculating Implementations from Specifications","author":"Backhouse Roland","year":"2003","unstructured":"Roland Backhouse. 2003. Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, Inc."},{"key":"e_1_3_1_5_1","doi-asserted-by":"crossref","unstructured":"Patrick Bahr. 2014. Proving Correctness of Compilers Using Structured Graphs. In Functional and Logic Programming (Lecture Notes in Computer Science Vol. 8475).","DOI":"10.1007\/978-3-319-07151-0_14"},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","unstructured":"Patrick Bahr and Graham Hutton. 2015. Calculating Correct Compilers. Journal of Functional Programming 25 (2015).","DOI":"10.1017\/S0956796815000180"},{"key":"e_1_3_1_7_1","doi-asserted-by":"crossref","unstructured":"Patrick Bahr and Graham Hutton. 2020. Calculating Correct Compilers II: Return of the Register Machines. Fournal of Functional Programming 30 (2020).","DOI":"10.1017\/S0956796820000209"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547624"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607855"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Patrick Bahr and Graham Hutton. 2024. Supplementary Material for \u201cBeyond Trees: Calculating Graph-Based Compilers\u201d. https:\/\/doi.org\/10.5281\/zenodo.11233589 10.5281\/zenodo.11233589","DOI":"10.5281\/zenodo.11233589"},{"key":"e_1_3_1_11_1","unstructured":"Lars Birkedal Ale\u0161 Bizjak Ranald Clouston Hans Bugge Grathwohl Bas Spitters and Andrea Vezzosi. 2016. Guarded Cubical Type Theory:Path Equality for Guarded Recursion. Schloss-Dagstuhl - Leibniz Zentrum f\u00fcr Informatik."},{"key":"e_1_3_1_12_1","volume-title":"Type-Driven Development with Idris","author":"Brady Edwin","year":"2017","unstructured":"Edwin Brady. 2017. Type-Driven Development with Idris. Manning Publications."},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","unstructured":"Venanzio Capretta. 2005. General Recursion via Coinductive Types. Logical Methods in Computer Science 1 2 (2005).","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_3_1_14_1","doi-asserted-by":"crossref","unstructured":"Adam Chlipala. 2008. Parametric Higher-Order Abstract Syntax for Mechanized Semantics. In Proceedings of the International Conference on Functional Programming.","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Nils Anders Danielsson. 2012. Operational Semantics Using the Partiality Monad. In Proceedings of the International Conference on Functional Programming.","DOI":"10.1145\/2364527.2364546"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13321-3_8"},{"issue":"5","key":"e_1_3_1_17_1","article-title":"Lambda Calculus Notation with Nameless Dummies, A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem","volume":"75","author":"de Bruijn N.G","year":"1972","unstructured":"N.G de Bruijn. 1972. Lambda Calculus Notation with Nameless Dummies, A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indagationes Mathematicae 75, 5 (1972).","journal-title":"Indagationes Mathematicae"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004075"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org\/2022\/6\/7"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"John Hughes Lars Pareto and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Proceedings of the 23rd Symposium on Principles of Programming Languages.","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_1_21_1","doi-asserted-by":"crossref","unstructured":"Graham Hutton and Patrick Bahr. 2017. Compiling a 50-Year Journey. Journal of Functional Programming 27 (2017).","DOI":"10.1017\/S0956796817000120"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_12"},{"key":"e_1_3_1_23_1","unstructured":"Yugo Kashiwagi and David Wise. 1991. Graph Algorithms in a Lazy Functional Programming Language."},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"David King and John Launchbury. 1995. Structuring Depth-First Search Algorithms in Haskell. In Proceedings of the 22nd Symposium on Principles of Programming Languages.","DOI":"10.1145\/199448.199530"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"John McCarthy and James Painter. 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":"e_1_3_1_28_1","volume-title":"Calculating Compilers","author":"Meijer Erik","year":"1992","unstructured":"Erik Meijer. 1992. Calculating Compilers. PhD Thesis. Katholieke Universiteit Nijmegen."},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","unstructured":"Andrey Mokhov. 2017. Algebraic Graphs with Class (Functional Pearl). In Proceedings of the 10th Symposium on Haskell.","DOI":"10.1145\/3122955.3122956"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290317"},{"key":"e_1_3_1_31_1","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science."},{"key":"e_1_3_1_32_1","volume-title":"Towards a Practical Programming Language Based on Dependent Type Theory","author":"Norell Ulf","year":"2007","unstructured":"Ulf Norell. 2007. Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis. Chalmers University of Technology."},{"key":"e_1_3_1_33_1","doi-asserted-by":"crossref","unstructured":"Bruno Oliveira and William Cook. 2012. Functional Programming with Structured Graphs. In Proceedings of the International Conference on Functional Programming.","DOI":"10.1145\/2364527.2364541"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473587"},{"key":"e_1_3_1_35_1","doi-asserted-by":"crossref","unstructured":"Norman Ramsey and Jo\u00e3o Dias. 2006. An Applicative Control-Flow Graph Based on Huet\u2019s Zipper. In Proceedings of the Workshop on ML.","DOI":"10.1016\/j.entcs.2005.11.042"},{"key":"e_1_3_1_36_1","doi-asserted-by":"crossref","unstructured":"Norman Ramsey Jo\u00e3o Dias and Simon Peyton Jones. 2010. Hoopl: A Modular Reusable Library for Dataflow Analysis and Transformation. In Proceedings of the Third Symposium on Haskell.","DOI":"10.1145\/1863523.1863539"},{"issue":"3","key":"e_1_3_1_37_1","article-title":"Deriving Target Code as a Representation of Continuation Semantics","volume":"4","author":"Wand Mitchell","year":"1982","unstructured":"Mitchell Wand. 1982. Deriving Target Code as a Representation of Continuation Semantics. ACM Transactions on Programming Languanges and Systems 4, 3 (1982).","journal-title":"ACM Transactions on Programming Languanges and Systems"},{"key":"e_1_3_1_38_1","doi-asserted-by":"crossref","unstructured":"Mitchell Wand. 1995. Compiler Correctness for Parallel Languages. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture.","DOI":"10.1145\/224164.224193"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:50:29Z","timestamp":1770191429000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":37,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674638"],"URL":"https:\/\/doi.org\/10.1145\/3674638","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}