Call-by-Value in a Basic Logic for Interaction

  • Ulrich Schöpp
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


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.


Free Variable Basic Logic Compilation Method Monoidal Category Source Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abramsky, S., Haghverdi, E., Scott, P.: Geometry of interaction and linear combinatory algebras. Mathematical Structures in Computer Science 12(5), 625–665 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 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)CrossRefGoogle Scholar
  4. 4.
    Appel, A.W.: Compiling with Continuations. Cambridge University Press (2006)Google Scholar
  5. 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)CrossRefGoogle Scholar
  6. 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. 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)CrossRefGoogle Scholar
  8. 8.
    Fischer, M.J.: Lambda calculus schemata. SIGACT News (14), 104–109 (1972)Google Scholar
  9. 9.
    Fredriksson, O., Ghica, D.R.: Abstract machines for game semantics, revisited. In: LICS, pp. 560–569. IEEE (2013)Google Scholar
  10. 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. 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. 12.
    Harper, R., Lillibridge, M.: Polymorphic type assignment and cps conversion. Lisp and Symbolic Computation 6(3-4), 361–380 (1993)CrossRefGoogle Scholar
  13. 13.
    Hatcliff, J., Danvy, O.: Thunks and the lambda-calculus. J. Funct. Program. 7(3), 303–319 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Honda, K., Yoshida, N.: Game-theoretic analysis of call-by-value computation. Theor. Comput. Sci. 221(1-2), 393–456 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. Cambridge Philos. Soc. 119(3), 447–468 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Laird, J.: Game semantics and linear cps interpretation. Theor. Comput. Sci. 333(1-2), 199–224 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Melliès, P.A.: Game semantics in string diagrams. In: LICS, pp. 481–490. IEEE (2012)Google Scholar
  18. 18.
    Melliès, P.A., Tabareau, N.: Resource modalities in game semantics. In: LICS, pp. 389–398 (2007)Google Scholar
  19. 19.
    Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 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)CrossRefGoogle Scholar
  21. 21.
    Schöpp, U.: Stratified bounded affine logic for logarithmic space. In: LICS, pp. 411–420 (2007)Google Scholar
  22. 22.
    Schöpp, U.: Computation-by-interaction with effects. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 305–321. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  23. 23.
    Schöpp, U.: On interaction, continuations and defunctionalization. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 205–220. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  24. 24.
    Schöpp, U.: Organising low-level programs using higher types. In: PPDP 2014 (to appear, 2014)Google Scholar
  25. 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. 26.
    Shao, Z., Appel, A.W.: Efficient and safe-for-space closure conversion. ACM Trans. Program. Lang. Syst. 22(1), 129–161 (2000)CrossRefGoogle Scholar
  27. 27.
    Wadler, P.: Theorems for free! In: FPCA, pp. 347–359 (1989)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Ulrich Schöpp
    • 1
  1. 1.Ludwig-Maximilians-Universität MünchenGermany

Personalised recommendations