[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Compilation of extended recursion in call-by-value functional languages

  • Published:
Higher-Order and Symbolic Computation

Abstract

This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than previous methods. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be correct.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Appel, A.W.: Compiling with Continuations. Cambridge University Press, Cambridge (1992)

    Google Scholar 

  2. Ariola, Z.M., Blom, S.: Skew confluence and the lambda calculus with letrec. Ann. Pure Appl. Log. 117(1–3), 95–178 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  3. Boudol, G.: The recursive record semantics of objects revisited. J. Funct. Program. 14(3), 263–315 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  4. Boudol, G., Zimmer, P.: Recursion in the call-by-value lambda-calculus. In: Ésik, Z., Ingólfsdóttir, A. (eds.) Fixed Points in Computer Science. BRICS Notes Series, vol. NS-02-2, pp. 61–66 (2002)

  5. Cardelli, L.: A semantics of multiple inheritance. In: Kahn, G., MacQueen, D., Plotkin, G. (eds.) Semantics of Data Types. Lecture Notes in Computer Science, vol. 173, pp. 51–67. Springer, Berlin (1984)

    Google Scholar 

  6. Cousineau, G., Curien, P.L., Mauny, M.: The categorical abstract machine. Sci. Comput. Program. 8(2), 173–202 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  7. Crary, K., Harper, R., Puri, S.: What is a recursive module? In: Programming Language Design and Implementation, pp. 50–63. ACM Press, New York (1999)

    Google Scholar 

  8. Dougherty, D.J., Lescanne, P., Liquori, L., Lang, F.: Addressed term rewriting systems: Syntax, semantics, and pragmatics: Extended abstract. In: Proceedings of the 2nd Int. Workshop on Term Graph Rewriting (TERMGRAPH 2004). Electr. Notes Theor. Comput. Sci., vol. 127(5), pp. 57–82. Elsevier, Amsterdam (2005)

    Google Scholar 

  9. Dreyer, D.: A type system for well-founded recursion. In: Principles of Programming Languages, pp. 293–305. ACM Press, New York (2004)

    Google Scholar 

  10. Dreyer, D.: A type system for recursive modules. In: International Conference on Functional Programming, pp. 289–302. ACM Press, New York (2007)

    Google Scholar 

  11. Erkök, L., Launchbury, J.: Recursive monadic bindings. In: International Conference on Functional Programming, pp. 174–185. ACM Press, New York (2000)

    Google Scholar 

  12. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Prentice-Hall, Englewood Cliffs (2005)

    Google Scholar 

  13. Hirschowitz, T.: Mixin modules, modules, and extended recursion in a call-by-value setting. Ph.D. thesis, University of Paris VII (2003)

  14. Hirschowitz, T.: Rigid mixin modules. In: Kameyama, Y., Stuckey, P. (eds.) Functional and Logic Programming. Lecture Notes in Computer Science, vol. 2998, pp. 214–228. Springer, Berlin (2004)

    Google Scholar 

  15. Hirschowitz, T., Leroy, X.: Mixin modules in a call-by-value setting. ACM Trans. Program. Lang. Syst. 27(5), 857–881 (2005)

    Article  Google Scholar 

  16. Hirschowitz, T., Leroy, X., Wells, J.B.: Compilation of extended recursion in call-by-value functional languages. In: Principles and Practice of Declarative Programming, pp. 160–171. ACM Press, New York (2003)

    Google Scholar 

  17. Hirschowitz, T., Leroy, X., Wells, J.B. Call-by-value mixin modules: Reduction semantics, side effects, types. In: Schmidt, D.A. (ed.) Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004. Lecture Notes in Computer Science, vol. 2986, pp. 64–78. Springer, Berlin (2004)

    Google Scholar 

  18. Kelsey, R., Clinger, W., Rees, J. (eds.): Revised5 report on the algorithmic language Scheme. Higher-Order Symb. Comput. 11(1), 7–105 (1998)

    Article  Google Scholar 

  19. Kranz, D., Kelsey, R., Rees, J., Hudak, P., Philbin, J., Adams, N.: ORBIT: An optimizing compiler for Scheme. In: Symposium on Compiler Construction, pp. 219–233. ACM Press, New York (1986)

    Google Scholar 

  20. Leroy, X., Doligez, D., Garrigue, J., Rémy, D., Vouillon, J.: The Objective Caml system release 3.11, documentation and user’s manual. Available at http://caml.inria.fr/pub/docs/manual-ocaml/ (2008)

  21. Leroy, X., Doligez, D., Garrigue, J., Vouillon, J.: The Objective Caml system. Software and documentation available at http://caml.inria.fr/ (1996–2009)

  22. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (revised). MIT Press, Cambridge (1997)

    Google Scholar 

  23. Moggi, E., Sabry, A.: An abstract monadic semantics for value recursion. Theor. Inf. Appl. 38(4), 375–400 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  24. Nordlander, J., Carlsson, M., Gill, A.: Unrestricted call-by-value recursion. In: ML’08: Proceedings of the 2008 ACM SIGPLAN workshop on ML, pp. 23–34. ACM Press, New York (2008)

    Chapter  Google Scholar 

  25. Peyton Jones, S. (ed.): Haskell 98 Language and Libraries, the revised report. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  26. Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  27. Russo, C.V.: Recursive structures for Standard ML. In: International Conference on Functional Programming, pp. 50–61. ACM Press, New York (2001)

    Google Scholar 

  28. Sewell, P., Stoyle, G., Hicks, M., Bierman, G., Wansbrough, K.: Dynamic rebinding for marshalling and update, via redex-time and destruct-time reduction. J. Funct. Program. 18(4), 437–502 (2008)

    MATH  MathSciNet  Google Scholar 

  29. Shivers, O.: Control-flow analysis in Scheme. In: Programming Language Design and Implementation, pp. 164–174. ACM Press, New York (1988)

    Google Scholar 

  30. Syme, D.: Initializing mutually referential abstract objects: The value recursion challenge. In: Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005). Electronic Notes in Theoretical Computer Science, vol. 148(2), pp. 3–25. Elsevier, Amsterdam (2006)

    Google Scholar 

  31. Waddell, O., Sarkar, D., Dybvig, R.K.: Fixing letrec: A faithful yet efficient implementation of Scheme’s recursive binding construct. Higher-Order Symb. Comput. 18(3/4), 299–326 (2005)

    Article  MATH  Google Scholar 

  32. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1992)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of Savoie, Campus Scientifique, 73376, Le Bourget-du-Lac, France

    Tom Hirschowitz

  2. INRIA Paris-Rocquencourt, Domaine de Voluceau, B.P. 105, 78153, Le Chesnay, France

    Xavier Leroy

  3. School of Mathematical and Computer Sciences, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, UK

    J. B. Wells

Authors
  1. Tom Hirschowitz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xavier Leroy
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. B. Wells
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tom Hirschowitz.

Additional information

Work partially supported by EPSRC grant GR/R 41545/01. This article is a revised and much extended version of [16].

Rights and permissions

Reprints and permissions

About this article

Cite this article

Hirschowitz, T., Leroy, X. & Wells, J.B. Compilation of extended recursion in call-by-value functional languages. Higher-Order Symb Comput 22, 3–66 (2009). https://doi.org/10.1007/s10990-009-9042-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10990-009-9042-z

Search

Navigation