Document Open Access Logo

Duality in Action (Invited Talk)

Authors Paul Downen , Zena M. Ariola

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.1.pdf
  • Filesize: 3.18 MB
  • 32 pages

Document Identifiers

Author Details

Paul Downen
  • Department of Computer & Information Science, University of Oregon, Eugene, OR, USA
Zena M. Ariola
  • Department of Computer & Information Science, University of Oregon, Eugene, OR, USA

Funding

This work is supported by the NSF under Grants No. 1719158 and No. 1423617.

Cite AsGet BibTex

Paul Downen and Zena M. Ariola. Duality in Action (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 1:1-1:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.1

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Duality
  • Logic
  • Curry-Howard
  • Sequent Calculus
  • Rewriting
  • Compilation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  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. Google Scholar
  2. Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992. Google Scholar
  3. L. E. J. Brouwer. Over de Grondslagen der Wiskunde. PhD thesis, University of Amsterdam, 1907. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. Paul Downen. Sequent Calculus: A Logic and a Language for Computation and Duality. PhD thesis, University of Oregon, 2017. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. Paul Downen and Zena M. Ariola. A tutorial on computational classical logic and the sequent calculus. Journal of Functional Programming, 28:e3, 2018. Google Scholar
  11. 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.
  12. 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. Google Scholar
  13. Paul Downen, Zena M. Ariola, and Silvia Ghilezan. The duality of classical intersection and union types. Fundamenta Informaticae, 170:1-54, 2019. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. 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. Google Scholar
  19. 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. Google Scholar
  20. M. Dummett and R. Minio. Elements of Intuitionism. Oxford University Press, 1977. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. Arend Heyting. Die formalen regeln der intuitionistischen logik. Sitzungsbericht PreuBische Akademie der Wissenschaften, pages 42-56, 1930. Google Scholar
  25. 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. Google Scholar
  26. 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. Google Scholar
  27. Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. Call-by-name extensionality and confluence. Journal of Functional Programming, 27:e12, 2017. Google Scholar
  28. 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. Google Scholar
  29. 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. Google Scholar
  30. Guillaume Munch-Maccagnoni. Syntax and Models of a non-Associative Composition of Programs and Proofs. PhD thesis, Université Paris Diderot, 2013. Google Scholar
  31. 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. Google Scholar
  32. 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. Google Scholar
  33. Noam Zeilberger. The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University, 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact