Document Open Access Logo

The Call-By-Value Lambda-Calculus with Generalized Applications

Author José Espírito Santo

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.35.pdf
  • Filesize: 451 kB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Lambda calculus
Keywords
  • Generalized applications
  • Natural deduction
  • Strong normalization
  • Standardization
  • Call-by-name
  • Call-by-value
  • Protecting-by-a-lambda

Metrics

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

Abstract

The lambda-calculus with generalized applications is the Curry-Howard counterpart to the system of natural deduction with generalized elimination rules for intuitionistic implicational logic. In this paper we identify a call-by-value variant of the system and prove confluence, strong normalization, and standardization. In the end, we show that the cbn and cbv variants of the system simulate each other via mappings based on extensions of the "protecting-by-a-lambda" compilation technique.

Cite As Get BibTex

José Espírito Santo. The Call-By-Value Lambda-Calculus with Generalized Applications. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 35:1-35:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.35

Author Details

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

Funding

The author was supported by Fundação para a Ciência e a Tecnologia (FCT) through project UID/MAT/00013/2013.

References

  1. B. Accattoli and G. Guerrieri. Open Call-by-Value. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 206-226, 2016. Google Scholar
  2. R. Dyckhoff and S. Lengrand. Call-by-value lambda calculus and LJQ. Journal of Logic and Computation, 17:1109-1134, 2007. Google Scholar
  3. J. Espírito Santo. Delayed substitutions. In Franz Baader, editor, Proceedings of RTA'07, volume 4533 of Lecture Notes in Computer Science, pages 169-183. Springer-Verlag, 2007. Google Scholar
  4. J. Espírito Santo. A note on preservation of strong normalisation in the λ-calculus. Theoretical Computer Science, 412(11):1027-1032, 2011. Google Scholar
  5. J. Espírito Santo, L. Pinto, and T. Uustalu. Modal Embeddings and Calling Paradigms. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany., volume 131 of LIPIcs, pages 18:1-18:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  6. G. Guerrieri, L. Paolini, and S. Ronchi Della Rocca. Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus. Logical Methods in Computer Science, 13(4), 2017. Google Scholar
  7. J. Hatcliff and O. Danvy. Thunks and the λ-Calculus (Extended Version). Technical Report BRICS RS-97-7, DIKU, 1997. Google Scholar
  8. F. Joachimski and R. 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
  9. E. Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, 1988. Google Scholar
  10. S. Negri and J. von Plato. Structural Proof Theory. Cambridge University Press, 2001. Google Scholar
  11. G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125-159, 1975. Google Scholar
  12. L. Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 126(2):281-292, 1994. Google Scholar
  13. A. Sabry and M. Felleisen. Reasoning about programms in continuation-passing-style. LISP and Symbolic Computation, 6(3/4):289-360, 1993. Google Scholar
  14. A. Sabry and P. Wadler. A reflection on call-by-value. ACM Trans. on Programming Languages and Systems, 19(6):916-941, 1997. Google Scholar
  15. M. Takahashi. Parallel reductions in λ-calculus. Information & Computation, 118:120-127, 1995. Google Scholar
  16. J. von Plato. Natural deduction with general elimination rules. Annals of Mathematical Logic, 40(7):541-567, 2001. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact