Grokking the Sequent Calculus (Functional Pearl)
Article No.: 250, Pages 395 - 425
Abstract
The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The 𝜆𝜇𝜇-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 𝜆𝜇𝜇-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 𝜆𝜇𝜇-calculus as a compiler intermediate language.
References
[1]
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 (POPL ’13). Association for Computing Machinery, New York, NY, USA. 27–38. isbn:9781450318327 https://doi.org/10.1145/2480359.2429075
[2]
Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation, 2 (1992), 297–347. https://doi.org/10.1093/logcom/2.3.297
[3]
David Binder, Marco Tzschentke, Marius Müller, and Klaus Ostermann. 2024. Grokking the Sequent Calculus (Functional Pearl). https://doi.org/10.5281/zenodo.12704905 Archived version of the submitted artefact
[4]
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 (2020), Article 126, nov, 30 pages. https://doi.org/10.1145/3428194
[5]
William R. Cook. 2009. On Understanding Data Abstraction, Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications: Onward! Essays. Association for Computing Machinery, New York, NY, USA. 557–572. https://doi.org/10.1145/1640089.1640133
[6]
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
[7]
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. isbn:978-3-642-15240-5
[8]
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
[9]
Paul Downen and Zena M. Ariola. 2018. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), Dan Ghica and Achim Jung (Eds.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 119). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 21:1–21:23. isbn:978-3-95977-088-0 issn:1868-8969 https://doi.org/10.4230/LIPIcs.CSL.2018.21
[10]
Paul Downen and Zena M. Ariola. 2018. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming, 28 (2018), https://doi.org/10.1017/S0956796818000023
[11]
Paul Downen and Zena M. Ariola. 2020. Compiling With Classical Connectives. Logical Methods in Computer Science, Volume 16, Issue 3 (2020), Aug., https://doi.org/10.23638/LMCS-16(3:13)2020
[12]
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 (ICFP 2015). Association for Computing Machinery, New York, NY, USA. 127–139. isbn:9781450336697 https://doi.org/10.1145/2784731.2784762
[13]
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.
[14]
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Codata in Action. In European Symposium on Programming (ESOP ’19). 119–146. https://doi.org/10.1007/978-3-030-17184-1_5
[15]
Matthias Felleisen. 1987. Reflections on Landin’s J-operator: A Partly Historical Note. Computer Languages, 12, 3 (1987), 197–207. issn:0096-0551 https://doi.org/10.1016/0096-0551(87)90022-1
[16]
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. issn:0304-3975 https://doi.org/10.1016/0304-3975(87)90109-5
[17]
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. isbn:354051662X
[18]
Gerhard Gentzen. 1935. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 35 (1935), 176–210.
[19]
Gerhard Gentzen. 1935. Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift, 39 (1935), 405–431.
[20]
Gerhard Gentzen. 1969. The collected papers of Gerhard Gentzen. North-Holland Publishing Co., Amsterdam.
[21]
Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science, 50, 1 (1987), 1–101. issn:0304-3975 https://doi.org/10.1016/0304-3975(87)90045-4
[22]
Brian Goetz. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https://jcp.org/en/jsr/detail?id=335
[23]
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 (POPL ’90). Association for Computing Machinery, New York, NY, USA. 47–58. https://doi.org/10.1145/96709.96714
[24]
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
[25]
Peter John Landin. 1965. Correspondence between ALGOL 60 and Church’s Lambda-notation: part I. Commun. ACM, 8, 2 (1965), feb, 89–101. issn:0001-0782 https://doi.org/10.1145/363744.363749
[26]
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. isbn:3540657630
[27]
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 (PLDI 2017). Association for Computing Machinery, New York, NY, USA. 482–494. isbn:9781450349888 https://doi.org/10.1145/3062341.3062380
[28]
Étienne Miquey. 2019. A Classical Sequent Calculus with Dependent Types. ACM Trans. Program. Lang. Syst., 41, 2 (2019), Article 8, mar, 47 pages. issn:0164-0925 https://doi.org/10.1145/3230625
[29]
Guillaume Munch-Maccagnoni. 2009. Focalisation and Classical Realisability. In Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Erich Grädel and Reinhard Kahle (Eds.) (CSL ’09). Springer, Berlin, Heidelberg. 409–423. https://doi.org/10.1007/978-3-642-04027-6_30
[30]
Guillaume Munch-Maccagnoni. 2013. Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph. D. Dissertation. Univ. Paris Diderot.
[31]
Sara Negri and Jan Von Plato. 2001. Structural Proof Theory. Cambridge University Press. https://doi.org/10.1017/CBO9780511527340
[32]
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 (2022), Article 106, 28 pages. https://doi.org/10.1145/3547637
[33]
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.
[34]
John Charles Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In ACMConf. Association for Computing Machinery, New York, NY, USA. 717–740. https://doi.org/10.1145/800194.805852
[35]
Arnaud Spiwack. 2014. A Dissection of L. Unpublished draft
[36]
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.
[37]
Hayo Thielecke. 1998. An Introduction to Landin‘s “A Generalization of Jumps and Labels”. Higher Order Symbol. Comput., 11, 2 (1998), sep, 117–123. issn:1388-3690 https://doi.org/10.1023/A:1010060315625
[38]
Anne Sjerp Troelstra and Helmut Schwichtenberg. 2000. Basic Proof Theory, Second Edition. Cambridge University Press.
[39]
Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods. North-Holland.
[40]
Philip Wadler. 2003. Call-by-value is dual to call-by-name. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP ’03). Association for Computing Machinery, New York, NY, USA. 189–201. isbn:1-58113-756-7 https://doi.org/10.1145/944705.944723
[41]
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, Jürgen Giesl (Ed.) (Lecture Notes in Computer Science, Vol. 3467). Springer, 185–203. https://doi.org/10.1007/978-3-540-32033-3_15
[42]
Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), 11, 38–94. issn:0890-5401 https://doi.org/10.1006/inco.1994.1093
[43]
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
[44]
Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching. Ph. D. Dissertation. Carnegie Mellon University. USA. isbn:9781109163018
[45]
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 (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 281–295. isbn:9781450342612 https://doi.org/10.1145/2908080.2908086
Index Terms
- Grokking the Sequent Calculus (Functional Pearl)
Recommendations
Sequent calculus as a compiler intermediate language
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingThe λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that would make for a good intermediate language, too? To ...
Sequent calculus as a compiler intermediate language
ICFP '16The λ-calculus is popular as an intermediate language for practical compilers. But in the world of logic it has a lesser-known twin, born at the same time, called the sequent calculus. Perhaps that would make for a good intermediate language, too? To ...
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer ApplicationsThe Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2024
1031 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 August 2024
Published in PACMPL Volume 8, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 153Total Downloads
- Downloads (Last 12 months)153
- Downloads (Last 6 weeks)144
Reflects downloads up to 26 Sep 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in