{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T17:10:20Z","timestamp":1723741820813},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,21]]},"abstract":"The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The \ud835\udf06\ud835\udf07\ud835\udf07-calculus is a term assignment system for the sequent calculus and a great foundation for compiler intermediate languages due to its first-class representation of evaluation contexts. Unfortunately, only experts of the sequent calculus can appreciate its beauty. To remedy this, we present the first introduction to the \ud835\udf06\ud835\udf07\ud835\udf07-calculus which is not directed at type theorists or logicians but at compiler hackers and programming-language enthusiasts. We do this by writing a compiler from a small but interesting surface language to the \ud835\udf06\ud835\udf07\ud835\udf07-calculus as a compiler intermediate language.<\/jats:p>","DOI":"10.1145\/3674639","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T16:49:04Z","timestamp":1723740544000},"page":"395-425","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Grokking the Sequent Calculus (Functional Pearl)"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"http:\/\/orcid.org\/0000-0003-1272-0972","authenticated-orcid":false,"given":"David","family":"Binder","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"ORCID":"http:\/\/orcid.org\/0009-0004-8834-2984","authenticated-orcid":false,"given":"Marco","family":"Tzschentke","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]},{"ORCID":"http:\/\/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"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-5294-5506","authenticated-orcid":false,"given":"Klaus","family":"Ostermann","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"David Binder Marco Tzschentke Marius M\u00fcller and Klaus Ostermann. 2024. Grokking the Sequent Calculus (Functional Pearl). https:\/\/doi.org\/10.5281\/zenodo.12704905 Archived version of the submitted artefact 10.5281\/zenodo.12704905","DOI":"10.5281\/zenodo.12704905"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640133"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351262"},{"key":"e_1_2_1_7_1","volume-title":"The Duality of Computation under Focus","author":"Curien Pierre-Louis","unstructured":"Pierre-Louis Curien and Guillaume Munch-Maccagnoni. 2010. The Duality of Computation under Focus. In Theoretical Computer Science, Cristian S. Calude and Vladimiro Sassone (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 165\u2013181. isbn:978-3-642-15240-5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_14"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2018.21"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000023"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(3:13)2020"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784762"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 74\u201388","author":"Downen Paul","year":"2016","unstructured":"Paul Downen, Luke Maurer, Zena M Ariola, and Simon Peyton Jones. 2016. Sequent calculus as a compiler intermediate language. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 74\u201388."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_5"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(87)90022-1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_2_1_17_1","volume-title":"Category Theory and Computer Science","author":"Filinski Andrzej","unstructured":"Andrzej Filinski. 1989. Declarative Continuations: an Investigation of Duality in Programming Language Semantics. In Category Theory and Computer Science. Springer-Verlag, Berlin, Heidelberg. 224\u2013249. isbn:354051662X"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen. I","volume":"35","author":"Gentzen Gerhard","year":"1935","unstructured":"Gerhard Gentzen. 1935. Untersuchungen \u00fcber das logische Schlie\u00dfen. I.. Mathematische Zeitschrift, 35 (1935), 176\u2013210.","journal-title":"Mathematische Zeitschrift"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"e_1_2_1_20_1","volume-title":"The collected papers of Gerhard Gentzen","author":"Gentzen Gerhard","unstructured":"Gerhard Gentzen. 1969. The collected papers of Gerhard Gentzen. North-Holland Publishing Co., Amsterdam."},{"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","unstructured":"Brian Goetz. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https:\/\/jcp.org\/en\/jsr\/detail?id=335"},{"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.1145\/363744.363749"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA \u201999)","author":"Levy Paul Blain","year":"1999","unstructured":"Paul Blain Levy. 1999. Call-by-Push-Value: A Subsuming Paradigm. In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA \u201999). Springer-Verlag, Berlin, Heidelberg. 228\u2013242. isbn:3540657630"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230625"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_30"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Guillaume Munch-Maccagnoni. 2013. Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph. D. Dissertation. Univ. Paris Diderot.","DOI":"10.1007\/978-3-642-54830-7_26"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547637"},{"key":"e_1_2_1_33_1","volume-title":"\u03bb \u03bc -Calculus: An algorithmic interpretation of classical natural deduction","author":"Parigot Michel","unstructured":"Michel Parigot. 1992. \u03bb \u03bc -Calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer, Berlin, Heidelberg. 190\u2013201."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_1_35_1","unstructured":"Arnaud Spiwack. 2014. A Dissection of L. Unpublished draft"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Morten Heine S\u00f8rensen and Pawe\u0142 Urzyczyn. 2006. Lectures on the Curry-Howard Isomorphism (Studies in Logic and the Foundations of Mathematics Vol. 149). Elsevier.","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010060315625"},{"key":"e_1_2_1_38_1","volume-title":"Basic Proof Theory","author":"Troelstra Anne Sjerp","unstructured":"Anne Sjerp Troelstra and Helmut Schwichtenberg. 2000. Basic Proof Theory, Second Edition. Cambridge University Press."},{"key":"e_1_2_1_39_1","unstructured":"Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_15"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2008.01.001"},{"key":"e_1_2_1_44_1","volume-title":"The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation","author":"Zeilberger Noam","unstructured":"Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation. Carnegie Mellon University. USA. isbn:9781109163018"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908086"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","deposited":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T16:53:38Z","timestamp":1723740818000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":45,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,21]]}},"alternative-id":["10.1145\/3674639"],"URL":"https:\/\/doi.org\/10.1145\/3674639","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}