Skip to main content
SpringerLink
Log in

Explicit Substitutions and Programming Languages

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1738))

Abstract

The λ-calculus has been much used to study the theory of substitution in logical systems and programming languages. However, with explicit substitutions, it is possible to get finer properties with respect to gradual implementations of substitutions as effectively done in runtimes of programming languages. But the theory of explicit substitutions has some defects such as non-confluence or the non-termination of the typed case. In this paper, we stress on the sub-theory of weak substitutions, which is sufficient to analyze most of the properties of programming languages, and which preserves many of the nice theorems of the λ-calculus.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 6(2):pp. 299–327, 1996. 181, 181

    Article  MathSciNet  Google Scholar 

  2. M. Abadi, B. Lampson, and J.-J. Lévy. Analysis and caching of dependencies. In Proc. of the 1996 ACM SIGPLAN International Conference on Functional Programming, pages pp. 83–91. ACM Press, May 1996. 198, 198

    Google Scholar 

  3. H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, 1981. 184, 192

    Google Scholar 

  4. Z.-E.-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. Lambda-upsilon, a calculus of explicit substitution which preserves strong normalisation. Research Report 2477, Inria, 1995. 181

    Google Scholar 

  5. G. Berry and J.-J. Lévy. Minimal and optima l computations of recursive programs. In Journal of the ACM, volume 26. ACM Press, 1979. 192

    Google Scholar 

  6. B. Blanchet. Escape analysis: Correctness proof, implementation and experimental results. In Proc. of 25th ACM Symposium on Principles of Programming Languages. ACM Press, 1998. 196, 198

    Google Scholar 

  7. R. Bloo and K. H. Rose. Combinatory reduction systems with explict substitutions thatpreserve strong normalization. In In Proc. of the 1996 confence on Rewriting Techniques and Applications. Springer, 1996. 181

    Google Scholar 

  8. N. Çağman and J. R. Hindley. Combinatory weak reduction in lambda calculus. Theoretical Computer Science, 198:pp. 239–249, 1998. 182, 183

    Article  MATH  MathSciNet  Google Scholar 

  9. G. Cousineau, P.-L. Curien, and M. Mauny. The categorical abstract machine. In Proc. of the second international conference on Functional programming languages and computer architecture. ACM Press, 1985. 182

    Google Scholar 

  10. P.-L. Curien. Categorical Combinator, Sequential Algorithms and Functional Programming. Pitman, 1986. 181

    Google Scholar 

  11. P.-L. Curien, T. Hardin, and J.-J. L’evy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):pp. 362–397, 1996. 181

    Article  MATH  MathSciNet  Google Scholar 

  12. R. David and B. Guillaume. The lambda I calculus. In Proc. of the Second International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 1999. 181

    Google Scholar 

  13. R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimitation in proof nets. In In Proc. of the 1997 symposium on Logics in Computer Science, 1997. 181

    Google Scholar 

  14. G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions: the case of higher-order patterns. In M. Maher, editor, In proc. of the joint international conference and symphosium on Logic Programming, 1996. 182

    Google Scholar 

  15. J. Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Proc. of the Seventeenth conference on Principles of Programming Languages, volume 6, pages pp. 1–15. ACM Press, 1990. 181, 198

    Google Scholar 

  16. G. Gonthier, M. Abadi, and J.-J. Lévy. The geometry of optimal lambda reduction. In Proc. of the Nineteenth conference on Principles of Programming Languages, volume 8. ACM Press, 1992. 196

    Google Scholar 

  17. T. Hardin. Confluence results for the pure strong categorical logic ccl. lambdacalculi as subsystems of ccl. Journal of Theoretical Computer Science, 65:291–342, 1989. 181

    Article  MATH  MathSciNet  Google Scholar 

  18. T. Hardin, L. Maranget, and B. Pagano. Functional runtimes within the lambdasigma calculus. Journal of Functional Programming, 8(2), march 1998. 198

    Google Scholar 

  19. J. R. Hindley. Combinatory reductions and lambda reductions compared. Zeit. Math. Logik, 23:pp. 169–180, 1977. 183

    Article  MATH  MathSciNet  Google Scholar 

  20. J.-W. Klop. Combinatory Reduction Systems. PhD thesis, Mathematisch Centrum, Amsterdam, 1980. 187

    MATH  Google Scholar 

  21. J. Launchbury. A natural semantics for lazy evaluation. In Proc. of the 1993 conference on Principles of Programming Languages. ACM Press, 1993. 194

    Google Scholar 

  22. X. Leroy. The ZINC experiment: an economical implementation of the ML language. Technical report 117, INRIA, 1990. 182, 196

    Google Scholar 

  23. P. Lescanne. From lambda-sigma to lambda-upsilon, a journey through calculi of explicit substitutions. In Proc. of the Twenty First conference on Principles of Programming Languages, 1994. 181

    Google Scholar 

  24. J.-J. Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Univ. of Paris 7, Paris, 1978. 192, 192

    Google Scholar 

  25. J.-J. Lévy. Optimal reductions in the lambda-calculus. In J. Seldin and J. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. Academic Press, 1980. On the occasion of his 80th birthday. 192, 192

    Google Scholar 

  26. L. Maranget. Optimal derivations in orthogonal term rewriting systems and in weak lambda calculi. In Proc. of the Eighteenth conference on Principles of Programming Languages. ACM Press, 1991. 192, 197

    Google Scholar 

  27. L. Maranget. La stratégie paresseuse. PhD thesis, Univ. of Paris 7, Paris, 1992. 192, 197

    Google Scholar 

  28. P.-A. Melli`es. Typed lambda-calculus with explicit substitutions may not terminate. In Proc. of the Second conference on Typed Lambda-Calculi and Applications. Springer, 1995. LNCS 902. 181

    Google Scholar 

  29. P.-A. Melli`es. Description Abstraite des Syst`emes de Réécriture. PhD thesis, Univ. of Paris 7, december 1996. 187, 188, 197

    Google Scholar 

  30. R. Milner. Action calculi and the pi-calculus. In Proc. of the NATO Summer School on Logic and Computation. Marktoberdorf, 1993. 182

    Google Scholar 

  31. S. L. Peyton-Jones. The implementation of Functional Programming Languages. Prentice-Hall, 1987. 197

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA - Rocquencourt, France

    Jean-Jacques Lévy & Luc Maranget

Authors
  1. Jean-Jacques Lévy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luc Maranget
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, Chennai, 600036, India

    C. Pandu Rangan

  2. Institute of Mathematical Sciences C.I.T. Campus, Chennai, 600113, India

    V. Raman  & R. Ramanujam  & 

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lévy, JJ., Maranget, L. (1999). Explicit Substitutions and Programming Languages. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1999. Lecture Notes in Computer Science, vol 1738. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46691-6_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-46691-6_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66836-7

  • Online ISBN: 978-3-540-46691-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation