Table of LinksIntroductionTranslating To Sequent Calculus2.1 Arithmetic Expressions2.2 Let Bindings2.3 Top-level Definitions2.4 Algebraic Data and Codata Types2.5 First-Class Functions2.6 Control OperatorsEvaluation Within a Context3.1 Evaluation Contexts for Fun3.2 Focusing on Evaluation in CoreTyping Rules4.1 Typing Rules for Fun4.2 Typing Rules for Core4.3 Type SoundnessInsights5.1 Evaluation Contexts are First Class5.2 Data is Dual to Codata5.3 Let-Bindings are Dual to Control Operators5.4 The Case-of-Case Transformation5.5 Direct and Indirect Consumers5.6 Call-By-Value, Call-By-Name and Eta-Laws5.7 Linear Logic and the Duality of ExceptionsRelated WorkConclusion, Data Availability Statement, and AcknowledgmentsA. The Relationship to the Sequent CalculusB. Typing Rules for FunC. Operational Semantics of label/gotoReferencesA The Relationship to the Sequent CalculusIn the main part of the paper we introduced the 𝜆𝜇𝜇˜-calculus without any references to the sequent calculus, because we think it is not essential to understand the latter in order to understand the former. In this appendix, we provide the details which help make the connection between the logical calculus and the term system clear. We only discuss a very simple sequent calculus which contains two logical connectives: the two conjunctions 𝐴 ⊗ 𝐵 and 𝐴 & 𝐵 which correspond to the strict and lazy pairs that we have seen in Core. We use 𝑋 for propositional variables.\𝐴, 𝐵 F 𝑋 | 𝐴 ⊗ 𝐵 | 𝐴 & 𝐵\In the (classical) sequent calculus both the premisses and the conclusion of a derivation rule consist of sequents Γ ⊢ Δ. Both Γ and Δ are multisets of formulas; that is, it is important how often a formula occurs on the left or the right, but not in which order the formulas occur. In the sequent calculus, we only have introduction rules. This means that the logically complex formula 𝐴 ⊗ 𝐵 or 𝐴 & 𝐵 only occurs in the conclusion of the rules that define it, and not in one of the premises. Every connective comes with a set of rules which introduce the connective on the left and the right of the turnstile. In our case, the rules look like this:\ \The rule Cut is the only rule which destroys the so-called subformula property. This property says that every formula which occurs anywhere in a derivation is a subformula of a formula occurring in the conclusion of the derivation. Proof theorists therefore try to show that we can eliminate the cuts; if every sequent which can be derived using the Cut rule can also be derived without using it, we say that the calculus enjoys the cut-elimination property. The Curry-Howard correspondence for the sequent calculus relates this cut-elimination procedure to the computations that we have seen in the paper.\The first step from the sequent calculus towards the 𝜆𝜇𝜇˜-calculus consists in marking at most one of the formulas in each of the sequents as active. We mark a formula as active by enclosing it in a pair of brackets. This yields two versions of the rule Axiom, one where we mark the formula on the left and one where we mark the formula on the right. If we want to translate every derivation using the original rules to a derivation in the new variant we also have to add special rules which activate and deactivate formulas both on the left and on the right. This yields the following new set of rules:\ B Typing Rules for FunGiven a term 𝑡, an environment Γ and a program 𝑃, if 𝑡 has type 𝜏 in environment Γ and program 𝑃, we write Γ ⊢𝑃 𝑡 : 𝜏. As 𝑃 is only used for typing calls to top-level definitions (rule Call), we usually leave it implicit in the typing rules. To make sure programs 𝑃 are well-formed, we have additional checking rules for programs ∅-ok and P-Ok. If a program is well-formed, we write ⊢ 𝑃 Ok.\\ \\\ \C Operational Semantics of label/gotoThe full operational semantics for the label/goto construct is in essence the same as for let/cc. To make it precise, we promote evaluation contexts to runtime values\We first repeat Definition 3.1 of evaluation contexts with one change: label 𝛼 {𝐸} is not an evaluation context. We reduce a label as soon as it comes into evaluation position.\\ \\Now we add them as another form of value\𝔱 F . . . | 𝐸\Note that these values only exist at runtime, that is, they cannot appear in expressions before evaluation has started. They are typed as consumers, which means that they are the only values with a consumer type. This makes sure that we can substitute them for covariables. Their typing can be captured by the following rule.\\ \\Now we can give the evaluation rules for label and goto:\𝐸[label 𝛼 {𝑡 }] ⊲ 𝐸[𝑡[𝐸/𝛼]] 𝐸 ′ [goto(𝔱; 𝐸)] ⊲ 𝐸[𝔱]\\ \\The rule for goto also is the reason why the theorem of strong preservation does not immediately hold (see the discussion in Section 4.3). The problem is that from this rule and the given typing rules for Fun it is not immediate that the evaluation contexts 𝐸 ′ and 𝐸 yield a term of the same type when filling their holes, so that the overall type of the term may not be preserved. But this cannot actually happen, because all other reduction rules preserve the overall type and hence all evaluation contexts that are reified by the rule for label must yield a term of that same overall type when their holes are filled. Therefore, also the rule for goto is type-preserving. This can be made precise by explicitly tracking the overall type in the type system (see, e.g., Section 6 in [Wright and Felleisen 1994]).ReferencesAndreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 27–38. https://doi.org/ 10.1145/2480359.2429075\Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation 2 (1992), 297–347. Issue 3. https://doi.org/10.1093/logcom/2.3.297\Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann. 2020. Effects as capabilities: effect handlers and lightweight effect polymorphism. Proc. ACM Program. Lang. 4, OOPSLA, Article 126 (nov 2020), 30 pages. https: //doi.org/10.1145/3428194\William R. Cook. 2009. On Understanding Data Abstraction, Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications: Onward! Essays (Orlando). Association for Computing Machinery, New York, NY, USA, 557–572. https://doi.org/10.1145/1640089.1640133\Pierre-Louis Curien and Hugo Herbelin. 2000. The Duality of Computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00). Association for Computing Machinery, New York, NY, USA, 233–243. https://doi.org/10.1145/357766.351262\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–181.\Paul Downen and Zena M. Ariola. 2014. The Duality of Construction. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410 (ESOP ’14). Springer, Berlin, Heidelberg, 249–269. https: //doi.org/10.1007/978-3-642-54833-8_14\Paul Downen and Zena M. Ariola. 2018a. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 119), Dan Ghica and Achim Jung (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 21:1–21:23. https://doi.org/10.4230/LIPIcs.CSL.2018.21\Paul Downen and Zena M. Ariola. 2018b. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming 28 (2018). https://doi.org/10.1017/S0956796818000023\Paul Downen and Zena M. Ariola. 2020. Compiling With Classical Connectives. Logical Methods in Computer Science Volume 16, Issue 3 (Aug. 2020). https://doi.org/10.23638/LMCS-16(3:13)2020\Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. 2015. Structures for structural recursion. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). Association for Computing Machinery, New York, NY, USA, 127–139. https://doi.org/10.1145/2784731.2784762\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–88.\Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Codata in Action. In European Symposium on Programming (ESOP ’19). Springer, 119–146. https://doi.org/10.1007/978-3-030-17184-1_5\Matthias Felleisen. 1987. Reflections on Landin’s J-operator: A Partly Historical Note. Computer Languages 12, 3 (1987), 197–207. https://doi.org/10.1016/0096-0551(87)90022-1\Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce Duba. 1987. A syntactic theory of sequential control. Theoretical Computer Science 52, 3 (1987), 205–237. https://doi.org/10.1016/0304-3975(87)90109-5\Andrzej Filinski. 1989. Declarative Continuations: an Investigation of Duality in Programming Language Semantics. In Category Theory and Computer Science. Springer-Verlag, Berlin, Heidelberg, 224–249.\Gerhard Gentzen. 1935a. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift 35 (1935), 176–210.\Gerhard Gentzen. 1935b. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift 39 (1935), 405–431.\Gerhard Gentzen. 1969. The collected papers of Gerhard Gentzen. North-Holland Publishing Co., Amsterdam.\Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50, 1 (1987), 1–101. https://doi.org/10.1016/0304- 3975(87)90045-4\Brian Goetz et al. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https://jcp.org/en/jsr/detail?id=335\Timothy G. Griffin. 1989. A Formulae-as-Type Notion of Control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, California, USA) (POPL ’90). Association for Computing Machinery, New York, NY, USA, 47–58. https://doi.org/10.1145/96709.96714\Tatsuya Hagino. 1989. Codatatypes in ML. Journal of Symbolic Computation 8, 6 (1989), 629–650. https://doi.org/10.1016/ S0747-7171(89)80065-3\Peter John Landin. 1965. Correspondence between ALGOL 60 and Church’s Lambda-notation: part I. Commun. ACM 8, 2 (feb 1965), 89–101. https://doi.org/10.1145/363744.363749\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 ’99). Springer-Verlag, Berlin, Heidelberg, 228–242.\Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. 2017. Compiling without Continuations. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain) (PLDI 2017). Association for Computing Machinery, New York, NY, USA, 482–494. https://doi.org/10.1145/3062341.3062380\Étienne Miquey. 2019. A Classical Sequent Calculus with Dependent Types. ACM Trans. Program. Lang. Syst. 41, 2, Article 8 (mar 2019), 47 pages. https://doi.org/10.1145/3230625\Guillaume Munch-Maccagnoni. 2009. Focalisation and Classical Realisability. In Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL (Coimbra, Portugal) (CSL ’09), Erich Grädel and Reinhard Kahle (Eds.). Springer, Berlin, Heidelberg, 409–423. https://doi.org/10.1007/978-3-642-04027-6_30\Guillaume Munch-Maccagnoni. 2013. Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph. D. Dissertation. Univ. Paris Diderot.\Sara Negri and Jan Von Plato. 2001. Structural Proof Theory. Cambridge University Press. https://doi.org/10.1017/ CBO9780511527340\Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen. 2022. Introduction and Elimination, Left and Right. Proc. ACM Program. Lang. 6, ICFP, Article 106 (2022), 28 pages. https://doi.org/10.1145/3547637\Michel Parigot. 1992. 𝜆𝜇-Calculus: An algorithmic interpretation of classical natural deduction. In Logic Programming and Automated Reasoning, Andrei Voronkov (Ed.). Springer, Berlin, Heidelberg, 190–201.\John Charles Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In ACMConf (Boston). Association for Computing Machinery, New York, NY, USA, 717–740. https://doi.org/10.1145/800194.805852\Arnaud Spiwack. 2014. A Dissection of L. (2014). Unpublished draft.\Morten Heine Sørensen and Paweł Urzyczyn. 2006. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, Vol. 149. Elsevier.\Hayo Thielecke. 1998. An Introduction to Landin‘s “A Generalization of Jumps and Labels”. Higher Order Symbol. Comput. 11, 2 (sep 1998), 117–123. https://doi.org/10.1023/A:1010060315625\Anne Sjerp Troelstra and Helmut Schwichtenberg. 2000. Basic Proof Theory, Second Edition. Cambridge University Press.\Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland.\Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (Uppsala, Sweden) (ICFP ’03). Association for Computing Machinery, New York, NY, USA, 189–201. https://doi.org/10.1145/944705.944723\Philip Wadler. 2005. Call-by-Value Is Dual to Call-by-Name - Reloaded. In Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings (Lecture Notes in Computer Science, Vol. 3467), Jürgen Giesl (Ed.). Springer, 185–203. https://doi.org/10.1007/978-3-540-32033-3_15\Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (11 1994), 38–94. https://doi.org/10.1006/inco.1994.1093\Noam Zeilberger. 2008. On the Unity of Duality. Annals of Pure and Applied Logic 153, 1-3 (2008), 66–96. https://doi.org/10. 1016/j.apal.2008.01.001\Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation. Carnegie Mellon University, USA. Advisor(s) Pfenning, Frank and Lee, Peter.\Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers. 2016. Accepting Blame for Safe Tunneled Exceptions. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (Santa Barbara, CA, USA) (PLDI ’16). Association for Computing Machinery, New York, NY, USA, 281–295. https://doi.org/10.1145/2908080.2908086\:::infoAuthors:(1) David Binder, University of Tübingen, Germany;(2) Marco Tzschentke, University of Tübingen, Germany;(3) Marius Muller, University of Tübingen, Germany;(4) Klaus Ostermann, University of Tübingen, Germany.::::::infoThis paper is available on arxiv under CC BY 4.0 license.:::\