{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:22Z","timestamp":1787592262267,"version":"build-2736575974"},"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\/legalcode"}],"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 high-level enough to allow for easy translation of surface languages into them and being low-level enough to make code generation easy. An intermediate representation based on a logical system typically has the former property and additionally satisfies several meta-theoretical properties which are valuable when optimizing code. Recently, classical sequent calculus, which is widely recognized and impactful within the fields of logic and proof theory, has been proposed as a natural candidate in this regard, due to its symmetric treatment of data and control flow. For such a language to be useful, however, it must eventually be compiled to machine code. In this paper, we introduce an intermediate representation that is based on classical sequent calculus and demonstrate that this language can be directly translated to conventional hardware. We provide both a formal description and an implementation. Preliminary performance evaluations indicate that our approach is 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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_12"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674639"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802799"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15240-5_13"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000023"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_14"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Paul Downen and Zena M Ariola. 2018. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming 28 (2018) e3. doi:10.1017\/S0956796818000023","DOI":"10.1017\/S0956796818000023"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(3:13)2020"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.1"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951931"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_5"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80065-3"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-97-2300-3_11"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/2738600.2738626"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291194"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547637"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236965"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000319"},{"key":"e_1_3_1_35_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. OpenJDK Project. HotSpot Group. https:\/\/cr.openjdk.org\/~rpressler\/loom\/Loom-Proposal.html"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784763"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9096-8"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_3_1_40_1","volume-title":"Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation. Extended Technical Report","author":"Schuster Philipp","year":"2025","unstructured":"Philipp Schuster, Marius M\u00fcller, Klaus Ostermann, and Jonathan Immanuel Brachth\u00e4user. 2025a. Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation. Extended Technical Report. University of T\u00fcbingen, Germany. https:\/\/se.informatik.uni-tuebingen.de\/publications\/schuster25compiling."},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Philipp Schuster Marius M\u00fcller Klaus Ostermann and Jonathan Immanuel Brachth\u00e4user. 2025b. Artifact of the paper \u2018Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation\u2019. doi:10.5281\/zenodo.14917573","DOI":"10.5281\/zenodo.14917573"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/889478"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_3_1_44_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. Technical Report UCB\/EECS-2014-54. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2014\/EECS-2014-54.html","DOI":"10.21236\/ADA605735"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/367593.367617"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/363156.363159"},{"key":"e_1_3_1_47_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":[[2026,8,24]],"date-time":"2026-08-24T16:32:15Z","timestamp":1787589135000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}