Duality in Action (Invited Talk)
The duality between "true" and "false" is a hallmark feature of logic. We show how this duality can be put to use in the theory and practice of programming languages and their implementations, too. Starting from a foundation of constructive logic as dialogues, we illustrate how it describes a symmetric language for computation, and survey several applications of the dualities found therein.
Duality
Logic
Curry-Howard
Sequent Calculus
Rewriting
Compilation
Theory of computation~Logic
1:1-1:32
Invited Talk
This work is supported by the NSF under Grants No. 1719158 and No. 1423617.
Paul
Downen
Paul Downen
Department of Computer & Information Science, University of Oregon, Eugene, OR, USA
https://www.pauldownen.com
https://orcid.org/0000-0003-0165-9387
Zena M.
Ariola
Zena M. Ariola
Department of Computer & Information Science, University of Oregon, Eugene, OR, USA
http://ix.cs.uoregon.edu/~ariola/
https://orcid.org/0000-0001-5551-8294
10.4230/LIPIcs.FSCD.2021.1
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming infinite structures by observations. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 27-38, 2013.
Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.
L. E. J. Brouwer. Over de Grondslagen der Wiskunde. PhD thesis, University of Amsterdam, 1907.
Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP '00, pages 233-243. ACM, 2000.
Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, 13(4):451-490, 1991.
Paul Downen. Sequent Calculus: A Logic and a Language for Computation and Duality. PhD thesis, University of Oregon, 2017.
Paul Downen and Zena M. Ariola. Compositional semantics for composable continuations: From abortive to delimited control. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP '14, pages 109-122. ACM, 2014.
Paul Downen and Zena M. Ariola. The duality of construction. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 249-269. Springer Berlin Heidelberg, 2014.
Paul Downen and Zena M. Ariola. Beyond polarity: Towards a multi-discipline intermediate language with sharing. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, LIPIcs, pages 21:1-21:23. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018.
Paul Downen and Zena M. Ariola. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming, 28:e3, 2018.
Paul Downen and Zena M. Ariola. Compiling with classical connectives. Logical Methods in Computer Science, 16:13:1-13:57, 2020. URL: http://arxiv.org/abs/1907.13227.
http://arxiv.org/abs/1907.13227
Paul Downen and Zena M. Ariola. A computational understanding of classical (co)recursion. In 22nd International Symposium on Principles and Practice of Declarative Programming, PPDP '20. Association for Computing Machinery, 2020.
Paul Downen, Zena M. Ariola, and Silvia Ghilezan. The duality of classical intersection and union types. Fundamenta Informaticae, 170:1-54, 2019.
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. Kinds are calling conventions. Proceedings of the ACM on Programming Languages, 4(ICFP), 2020.
Paul Downen, Philip Johnson-Freyd, and Zena Ariola. Abstracting models of strong normalization for classical calculi. Journal of Logical and Algebraic Methods in Programming, 111, 2019.
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. Structures for structural recursion. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 127-139. ACM, 2015.
Paul Downen, Luke Maurer, Zena M. Ariola, and Simon Peyton Jones. Sequent calculus as a compiler intermediate language. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 74-88. ACM, 2016.
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. Codata in action. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 119-146. Springer International Publishing, 2019.
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. Making a faster curry with extensional types. In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell 2019, pages 58-70. ACM, 2019.
M. Dummett and R. Minio. Elements of Intuitionism. Oxford University Press, 1977.
Richard A. Eisenberg and Simon Peyton Jones. Levity polymorphism. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, page 525–539. Association for Computing Machinery, 2017.
Jean-Yves Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination de coupures dans l'analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the 2nd Scandinavian Logic Symposium, pages 63-92. North-Holland, 1971.
Timothy G. Griffin. A formulae-as-types notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 47-58. ACM, 1990.
Arend Heyting. Die formalen regeln der intuitionistischen logik. Sitzungsbericht PreuBische Akademie der Wissenschaften, pages 42-56, 1930.
William Alvin Howard. The formulae-as-types notion of construction. In Haskell Curry, Hindley B., Seldin J. Roger, and P. Jonathan, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.
Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. First class call stacks: Exploring head reduction. In Workshop on Continuations, volume 212 of WOC, 2015.
Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. Call-by-name extensionality and confluence. Journal of Functional Programming, 27:e12, 2017.
Jan W. Klop and Roel C. de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, 80(2):97-113, 1989.
Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. Compiling without continuations. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 482-494. ACM, 2017.
Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Université Paris Diderot, 2013.
Michel Parigot. Lambda-my-calculus: An algorithmic interpretation of classical natural deduction. In Proceedings of the International Conference on Logic Programming and Automated Reasoning, LPAR '92, pages 190-201. Springer-Verlag, 1992.
Simon L. Peyton Jones and John Launchbury. Unboxed values as first class citizens in a non-strict functional language. In Functional Programming Languages and Computer Architecture, 5th ACM Conference, Cambridge, MA, USA, August 26-30, 1991, Proceedings, volume 523 of Lecture Notes in Computer Science, pages 636-666. Springer-Verlag, 1991.
Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University, 2009.
Paul Downen and Zena M. Ariola
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode