{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:10:46Z","timestamp":1760058646280,"version":"build-2065373602"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["448316946"],"award-info":[{"award-number":["448316946"]}],"id":[{"id":"10.13039\/501100001659","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":[[2025,4,9]]},"abstract":"<jats:p>Compiler intermediate representations have to strike a balance between being\n \n \n \nhigh-level enough to allow for easy translation of surface languages into them\n \n \n \nand being low-level enough to make code generation easy. An intermediate representation\n \n \n \nbased on a logical system typically has the former property and additionally satisfies\n \n \n \nseveral meta-theoretical properties which are valuable when optimizing code.\n \n \n \nRecently, classical sequent calculus, which is widely recognized and impactful within the\n \n \n \nfields of logic and proof theory, has been proposed as a natural candidate in\n \n \n \nthis regard, due to its symmetric treatment of data and control flow. For\n \n \n \nsuch a language to be useful, however, it must eventually be compiled to machine\n \n \n \ncode. In this paper, we introduce an intermediate representation that is based\n \n \n \non classical sequent calculus and demonstrate that this language can be directly\n \n \n \ntranslated to conventional hardware. We provide both a formal description and an\n \n \n \nimplementation. Preliminary performance evaluations indicate that our approach\n \n \n \nis viable.<\/jats:p>","DOI":"10.1145\/3720507","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1746-1773","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8011-0506","authenticated-orcid":false,"given":"Philipp","family":"Schuster","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0260-6298","authenticated-orcid":false,"given":"Marius","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5294-5506","authenticated-orcid":false,"given":"Klaus","family":"Ostermann","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_12"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674639"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802799"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000023"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_14"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000023"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(3:13)2020"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951931"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_5"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80065-3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-97-2300-3_11"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2738600.2738626"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291194"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547637"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236965"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000319"},{"key":"e_1_2_1_34_1","volume-title":"Loom Project: Fibers and Continuations for the Java Virtual Machine","author":"Pressler Ron","year":"2017","unstructured":"Ron Pressler. 2017. Loom Project: Fibers and Continuations for the Java Virtual Machine. HotSpot Group. https:\/\/cr.openjdk.org\/~rpressler\/loom\/Loom-Proposal.html"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784763"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9096-8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"volume-title":"Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation","author":"Schuster Philipp","key":"e_1_2_1_39_1","unstructured":"Philipp Schuster, Marius M\u00fcller, Klaus Ostermann, and Jonathan Immanuel Brachth\u00e4user. 2025. Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation. University of T\u00fcbingen, Germany. https:\/\/se.informatik.uni-tuebingen.de\/publications\/schuster25compiling"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Philipp Schuster Marius M\u00fcller Klaus Ostermann and Jonathan Immanuel Brachth\u00e4user. 2025. Artifact of the paper \u2019Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation\u2019. https:\/\/doi.org\/10.5281\/zenodo.14917573 10.5281\/zenodo.14917573","DOI":"10.5281\/zenodo.14917573"},{"key":"e_1_2_1_41_1","volume-title":"Rabbit: A Compiler for Scheme. USA. https:\/\/hdl.handle.net\/1721.1\/6913","author":"Steele Guy L.","year":"1978","unstructured":"Guy L. Steele. 1978. Rabbit: A Compiler for Scheme. USA. https:\/\/hdl.handle.net\/1721.1\/6913"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Andrew Waterman Yunsup Lee David A. Patterson and Krste Asanovi\u0107. 2014. The RISC-V Instruction Set Manual Volume I: User-Level ISA Version 2.0. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2014\/EECS-2014-54.html","DOI":"10.21236\/ADA605735"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/367593.367617"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/363156.363159"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720507","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720507","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:14:42Z","timestamp":1760030082000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720507"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":46,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720507"],"URL":"https:\/\/doi.org\/10.1145\/3720507","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}