Document Open Access Logo

Standardization of a Call-By-Value Lambda-Calculus

Authors Giulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca

PDF

File

Thumbnail PDF
PDF
LIPIcs.TLCA.2015.211.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • standardization,sequentialization,lambda-calculus,sigma-reduction,par- allel reduction
  • call-by-value
  • head reduction
  • internal reduction
  • solvability

Metrics

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

Abstract

We study an extension of Plotkin's call-by-value lambda-calculus by means of two commutation rules (sigma-reductions). Recently, it has been proved that this extended calculus provides elegant characterizations of many semantic properties, as for example solvability. We prove a standardization theorem for this calculus by generalizing Takahashi's approach of parallel reductions. The standardization property allows us to prove that our calculus is conservative with respect to the Plotkin's one. In particular, we show that the notion of solvability for this calculus coincides with that for Plotkin's call-by-value lambda-calculus.

Cite As Get BibTex

Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 211-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.211

Author Details

Giulio Guerrieri
Luca Paolini
Simona Ronchi Della Rocca

References

  1. Beniamino Accattoli and Luca Paolini. Call-by-Value Solvability, Revisited. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming, volume 7294 of Lecture Notes in Computer Science, pages 4-16. Springer-Verlag, 2012. Google Scholar
  2. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North Holland, 1984. Google Scholar
  3. Alberto Carraro and Giulio Guerrieri. A Semantical and Operational Account of Call-by-Value Solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer-Verlag, 2014. Google Scholar
  4. Karl Crary. A Simple Proof of Call-by-Value Standardization. Technical Report CMU-CS-09-137, Carnegie Mellon University, 2009. Google Scholar
  5. Haskell B. Curry and Robert Feys. Combinatory Logic, volume 1. North Holland, 1958. Google Scholar
  6. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  7. Hugo Herbelin and Stéphane Zimmermann. An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 142-156. Springer-Verlag, 2009. Google Scholar
  8. Roger Hindley. Standard and normal reductions. Transactions of the American Mathematical Society, pages 253-271, 1978. Google Scholar
  9. 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
  10. Eugenio Moggi. Computational Lambda-Calculus and Monads. In Logic in Computer Science, pages 14-23. IEEE Computer Society, 1989. Google Scholar
  11. Luca Paolini. Call-by-Value Separability and Computability. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Italian Conference in Theoretical Computer Science, volume 2202 of Lecture Notes in Computer Science, pages 74-89. Springer-Verlag, 2002. Google Scholar
  12. Luca Paolini and Simona Ronchi Della Rocca. Parametric parameter passing lambda-calculus. Information and Computation, 189(1):87-106, 2004. Google Scholar
  13. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value Solvability. Theoretical Informatics and Applications, 33(6):507-534, 1999. RAIRO Series, EDP-Sciences. Google Scholar
  14. Luca Paolini and Simona Ronchi Della Rocca. The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer-Verlag, 2004. Google Scholar
  15. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. Google Scholar
  16. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and symbolic computation, 6(3-4):289-360, 1993. Google Scholar
  17. Masako Takahashi. Parallel reductions in lambda-calculus. Information and Computation, 118(1):120-127, 1995. 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