Table of Links Introduction


Translating To Sequent Calculus
2.1 Arithmetic Expressions
2.2 Let Bindings
2.3 Top-level Definitions
2.4 Algebraic Data and Codata Types
2.5 First-Class Functions
2.6 Control Operators


Evaluation Within a Context
3.1 Evaluation Contexts for Fun
3.2 Focusing on Evaluation in Core


Typing Rules
4.1 Typing Rules for Fun
4.2 Typing Rules for Core
4.3 Type Soundness


Insights
5.1 Evaluation Contexts are First Class
5.2 Data is Dual to Codata
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
5.6 Call-By-Value, Call-By-Name and Eta-Laws
5.7 Linear Logic and the Duality of Exceptions


Related Work


Conclusion, Data Availability Statement, and Acknowledgments Introduction Introduction Introduction Introduction Translating To Sequent Calculus
2.1 Arithmetic Expressions
2.2 Let Bindings
2.3 Top-level Definitions
2.4 Algebraic Data and Codata Types
2.5 First-Class Functions
2.6 Control Operators Translating To Sequent Calculus Translating To Sequent Calculus 2.1 Arithmetic Expressions 2.1 Arithmetic Expressions 2.2 Let Bindings 2.2 Let Bindings 2.3 Top-level Definitions 2.3 Top-level Definitions 2.4 Algebraic Data and Codata Types 2.4 Algebraic Data and Codata Types 2.5 First-Class Functions 2.5 First-Class Functions 2.6 Control Operators 2.6 Control Operators Evaluation Within a Context
3.1 Evaluation Contexts for Fun
3.2 Focusing on Evaluation in Core Evaluation Within a Context Evaluation Within a Context 3.1 Evaluation Contexts for Fun 3.1 Evaluation Contexts for Fun 3.2 Focusing on Evaluation in Core 3.2 Focusing on Evaluation in Core Typing Rules
4.1 Typing Rules for Fun
4.2 Typing Rules for Core
4.3 Type Soundness Typing Rules Typing Rules Typing Rules 4.1 Typing Rules for Fun 4.1 Typing Rules for Fun 4.2 Typing Rules for Core 4.2 Typing Rules for Core 4.3 Type Soundness 4.3 Type Soundness Insights
5.1 Evaluation Contexts are First Class
5.2 Data is Dual to Codata
5.3 Let-Bindings are Dual to Control Operators
5.4 The Case-of-Case Transformation
5.5 Direct and Indirect Consumers
5.6 Call-By-Value, Call-By-Name and Eta-Laws
5.7 Linear Logic and the Duality of Exceptions Insights Insights 5.1 Evaluation Contexts are First Class 5.1 Evaluation Contexts are First Class 5.2 Data is Dual to Codata 5.2 Data is Dual to Codata 5.3 Let-Bindings are Dual to Control Operators 5.3 Let-Bindings are Dual to Control Operators 5.4 The Case-of-Case Transformation 5.4 The Case-of-Case Transformation 5.5 Direct and Indirect Consumers 5.5 Direct and Indirect Consumers 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.6 Call-By-Value, Call-By-Name and Eta-Laws 5.7 Linear Logic and the Duality of Exceptions 5.7 Linear Logic and the Duality of Exceptions Related Work Related Work Related Work Related Work Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments Conclusion, Data Availability Statement, and Acknowledgments A. The Relationship to the Sequent Calculus A. The Relationship to the Sequent Calculus B. Typing Rules for Fun B. Typing Rules for Fun C. Operational Semantics of label/goto C. Operational Semantics of label/goto References References A The Relationship to the Sequent Calculus In 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 Fun Given 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/goto The 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]). References Andreas 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 Authors:
(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. Authors: Authors: (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. This paper is available on arxiv under CC BY 4.0 license. This paper is available on arxiv under CC BY 4.0 license. available on arxiv available on arxiv

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Notion

What Codata, Control Flow, and Logic Teach Us About Programming

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

What Sequent Calculus Teaches Us About Computation

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Account Abstraction, Analysed: Abstract & Introduction

Rules of Thumb for Software Engineering

Building a cupboard

What is Code Review and Why We Need to Keep Doing It

How to Find the Stinky Parts of Your Code: 251 - Empty Collections

Account Abstraction, Analysed: Abstract & Introduction

Rules of Thumb for Software Engineering

Building a cupboard

What is Code Review and Why We Need to Keep Doing It

How to Find the Stinky Parts of Your Code: 251 - Empty Collections

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps