Call-by-Value in a Basic Logic for Interaction | SpringerLink
Skip to main content
Springer Nature Link
Log in

Call-by-Value in a Basic Logic for Interaction

  • Conference paper
Programming Languages and Systems (APLAS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8858))

Included in the following conference series:

Abstract

In game semantics and related approaches to programming language semantics, programs are modelled by interaction dialogues. Such models have recently been used by a number of authors for the design of compilation methods, in particular for applications where resource control is important. The work in this area has focused on call-by-name languages. In this paper we study the compilation of call-by-value into a first-order low-level language by means of an interpretation in a semantic interactive model. We refine the methods developed for call-by-name languages to allow an efficient treatment of call-by-value. We introduce an intermediate language that is based on the structure of an interactive computation model and that can be seen as a fragment of Linear Logic. The main result is that Plotkin’s call-by-value cps-translation and its soundness proof can be refined to target this intermediate language. This refined cps-translation amounts to a direct compilation of the source language into a first-order language.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

  1. Abramsky, S., Haghverdi, E., Scott, P.: Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science 12(5), 625–665 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  3. Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Appel, A.W.: Compiling with Continuations. Cambridge University Press (2006)

    Google Scholar 

  5. Banerjee, A., Heintze, N., Riecke, J.G.: Design and correctness of program transformations based on control-flow analysis. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 420–447. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Cejtin, H., Jagannathan, S., Weeks, S.: Flow-directed closure conversion for typed languages. In: Smolka, G. (ed.) ESOP/ETAPS 2000. LNCS, vol. 1782, pp. 56–71. Springer, Heidelberg (2000)

    Google Scholar 

  7. Dal Lago, U., Schöpp, U.: Functional programming in sublinear space. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 205–225. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Fischer, M.J.: Lambda calculus schemata. SIGACT News (14), 104–109 (1972)

    Google Scholar 

  9. Fredriksson, O., Ghica, D.R.: Abstract machines for game semantics, revisited. In: LICS, pp. 560–569. IEEE (2013)

    Google Scholar 

  10. Ghica, D.R.: Geometry of synthesis: A structured approach to VLSI design. In: Hofmann, M., Felleisen, M. (eds.) POPL, pp. 363–375. ACM (2007)

    Google Scholar 

  11. Ghica, D.R., Smith, A., Singh, S.: Geometry of synthesis IV: Compiling affine recursion into static hardware. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP, pp. 221–233 (2011)

    Google Scholar 

  12. Harper, R., Lillibridge, M.: Polymorphic type assignment and cps conversion. Lisp and Symbolic Computation 6(3-4), 361–380 (1993)

    Article  Google Scholar 

  13. Hatcliff, J., Danvy, O.: Thunks and the lambda-calculus. J. Funct. Program. 7(3), 303–319 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  14. Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation. Theor. Comput. Sci. 221(1-2), 393–456 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  15. Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. Cambridge Philos. Soc. 119(3), 447–468 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  16. Laird, J.: Game semantics and linear cps interpretation. Theor. Comput. Sci. 333(1-2), 199–224 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  17. Melliès, P.A.: Game semantics in string diagrams. In: LICS, pp. 481–490. IEEE (2012)

    Google Scholar 

  18. Melliès, P.A., Tabareau, N.: Resource modalities in game semantics. In: LICS, pp. 389–398 (2007)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  20. Plotkin, G.D., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  21. Schöpp, U.: Stratified bounded affine logic for logarithmic space. In: LICS, pp. 411–420 (2007)

    Google Scholar 

  22. Schöpp, U.: Computation-by-interaction with effects. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 305–321. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  23. Schöpp, U.: On interaction, continuations and defunctionalization. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 205–220. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  24. Schöpp, U.: Organising low-level programs using higher types. In: PPDP 2014 (to appear, 2014)

    Google Scholar 

  25. Selinger, P.: A survey of graphical languages for monoidal categories. In: New Structures for Physics. Lecture Notes in Physics, vol. 813, pp. 289–355. Springer (2011)

    Google Scholar 

  26. Shao, Z., Appel, A.W.: Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. 22(1), 129–161 (2000)

    Article  Google Scholar 

  27. Wadler, P.: Theorems for free! In: FPCA, pp. 347–359 (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Ludwig-Maximilians-Universität München, Germany

    Ulrich Schöpp

Authors
  1. Ulrich Schöpp
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Graduate School of Mathematics, Nagoya University, 464-8602, Chikusa-ku, Nagoya, Japan

    Jacques Garrigue

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Schöpp, U. (2014). Call-by-Value in a Basic Logic for Interaction. In: Garrigue, J. (eds) Programming Languages and Systems. APLAS 2014. Lecture Notes in Computer Science, vol 8858. Springer, Cham. https://doi.org/10.1007/978-3-319-12736-1_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12736-1_23

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12735-4

  • Online ISBN: 978-3-319-12736-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics