Document Open Access Logo

The Logical Essence of Compiling with Continuations

Authors José Espírito Santo , Filipa Mendes

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.19.pdf
  • Filesize: 0.75 MB
  • 21 pages

Document Identifiers

Author Details

José Espírito Santo
  • Centre of Mathematics, University of Minho, Portugal
Filipa Mendes
  • Centre of Mathematics, University of Minho, Portugal

Funding

The first author was partially financed by Portuguese Funds through FCT (Fundação para a Ciência e a Tecnologia) within the Projects UIDB/00013/2020 and UIDP/00013/2020.

Cite AsGet BibTex

José Espírito Santo and Filipa Mendes. The Logical Essence of Compiling with Continuations. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.19

Abstract

The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lambda-calculus (λ{𝖢}), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the "essence" of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of λ{𝖢}, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Operational semantics
  • Theory of computation → Type structures
Keywords
  • Continuation-passing style
  • Sequent calculus
  • Generalized applications
  • Administrative normal form

Metrics

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

Related Versions

References

  1. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, SIGPLAN Notices 35(9), pages 233-243. ACM, 2000. URL: https://doi.org/10.1145/351240.351262.
  2. Paul Downen, Luke Maurer, Zena M. Ariola, and Simon Peyton Jones. Sequent calculus as a compiler intermediate language. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 74-88. ACM, 2016. Google Scholar
  3. Roy Dyckhoff and Stéphane Lengrand. LJQ, a strongly focused calculus for intuitionistic logic. In A. Beckmann, U. Berger, B. Löwe, and J. V Tucker, editors, Proc. of the 2nd Conference on Computability in Europe (CiE'06), volume 3988 of Lecture Notes in Computer Science. Springer-Verlag, 2006. Google Scholar
  4. Roy Dyckhoff and Stéphane Lengrand. Call-by-value lambda calculus and LJQ. Journal of Logic and Computation, 17:1109-1134, 2007. Google Scholar
  5. José Espírito Santo. Towards a canonical classical natural deduction system. Annals of Pure and Applied Logic, 164(6):618-650, 2013. Google Scholar
  6. José Espírito Santo. The call-by-value lambda-calculus with generalized applications. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 35:1-35:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  7. José Espírito Santo and Filipa Mendes. The logical essence of compiling with continuations. CoRR, 2023. URL: https://arxiv.org/2304.14752.
  8. José Espírito Santo. The λ-calculus and the unity of structural proof theory. Theory of Computing Systems, 45:963-994, 2009. Google Scholar
  9. José Espírito Santo, Ralph Matthes, and Luís Pinto. Continuation-passing-style and strong normalization for intuitionistic sequent calculi. Logical Methods in Computer Science, 5(2:11), 2009. Google Scholar
  10. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Robert Cartwright, editor, Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, pages 237-247. ACM, 1993. Google Scholar
  11. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations (with retrospective). In Kathryn S. McKinley, editor, 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection, pages 502-514. ACM, 2003. Google Scholar
  12. Timothy G. Griffin. A formulae-as-types notion of control. In ACM Conf. Principles of Programming Languages. ACM Press, 1990. Google Scholar
  13. Hugo Herbelin. A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, Proceedings of CSL'94, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer-Verlag, 1995. Google Scholar
  14. Hugo Herbelin and Stéphane Zimmermann. An operational account of call-by-value minimal and classical lambda-calculus in "natural deduction" form. In Proceedings of Typed Lambda Calculi and Applications'09, volume 5608 of LNCS, pages 142-156. Springer-Verlag, 2009. Google Scholar
  15. Felix Joachimski and Ralph Matthes. Standardization and confluence for a lambda calculus with generalized applications. In Proceedings of RTA 2000, volume 1833 of LNCS, pages 141-155. Springer, 2000. Google Scholar
  16. Andrew Kennedy. Compiling with continuations, continued. In Ralf Hinze and Norman Ramsey, editors, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, October 1-3, 2007, pages 177-190. ACM, 2007. Google Scholar
  17. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theoretical Computer Science, 228(1-2):175-210, 1999. Google Scholar
  18. Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. Compiling without continuations. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 482-494. ACM, 2017. Google Scholar
  19. Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs, Conference, Brooklyn College, New York, NY, USA, June 17-19, 1985, Proceedings, volume 193 of Lecture Notes in Computer Science, pages 219-224. Springer, 1985. Google Scholar
  20. Eugenio Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, 1988. Google Scholar
  21. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. Google Scholar
  22. M. Parigot. λμ-calculus: an algorithmic interpretation of classic natural deduction. In Int. Conf. Logic Prog. Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer Verlag, 1992. Google Scholar
  23. Gordon Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125-159, 1975. Google Scholar
  24. Amr Sabry and Matthias Felleisen. Reasoning about programms in continuation-passing-style. LISP and Symbolic Computation, 6(3/4):289-360, 1993. Google Scholar
  25. Amr Sabry and Philip Wadler. A reflection on call-by-value. ACM Trans. on Programming Languages and Systems, 19(6):916-941, 1997. Google Scholar
  26. Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry/Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. Google Scholar
  27. Philip Wadler. Call-by-value is dual to call-by-name. In Colin Runciman and Olin Shivers, editors, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, ICFP 2003, Uppsala, Sweden, August 25-29, 2003, pages 189-201. ACM, 2003. 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