1. Beniamino Accattoli (2011): Jumping around the box: graphical and operational studies on λ-calculus and Linear Logic. PhD thesis. La Sapienza University of Rome.
  2. Beniamino Accattoli (2012): A linear analysis of call-by-value λ-calculus. Available at the address
  3. Beniamino Accattoli & Stefano Guerrini (2009): Jumping Boxes. In: CSL, pp. 55–70. Available at
  4. Beniamino Accattoli & Delia Kesner (2010): The Structural λ-Calculus. In: CSL, pp. 381–395. Available at
  5. Beniamino Accattoli & Luca Paolini (2012): Call-by-Value Solvability, revisited. In: FLOPS, pp. 4–16. Available at
  6. Roberto Di Cosmo & Delia Kesner (1997): Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract). In: LICS, pp. 35–46. Available at
  7. Roberto Di Cosmo, Delia Kesner & Emmanuel Polonovski (2003): Proof Nets And Explicit Substitutions. Math. Str. in Comput. Sci. 13(3), pp. 409–450. Available at
  8. Vincent Danos (1990): La Logique Linéaire appliqué à l'étude de divers processus de normalisation (principalment du λ-calcul). Phd thesis. Université Paris 7.
  9. Vincent Danos & Laurent Regnier (1995): Proof-nets and the Hilbert space. In: Advances in Linear Logic. Cambridge University Press, pp. 307–328. Available at
  10. Vincent Danos & Laurent Regnier (1999): Reversible, Irreversible and Optimal lambda-Machines. Theor. Comput. Sci. 227(1-2), pp. 79–97. Available at
  11. Maribel Fernández & Ian Mackie (2002): Call-by-Value lambda-Graph Rewriting Without Rewriting. In: ICGT, pp. 75–89. Available at
  12. Maribel Fernández & Nikolaos Siafakas (2009): Labelled Lambda-calculi with Explicit Copy and Erase. In: LINEARITY, pp. 49–64. Available at
  13. Cormac Flanagan, Amr Sabry, Bruce F. Duba & Matthias Felleisen (1993): The Essence of Compiling with Continuations. In: PLDI, pp. 237–247. Available at
  14. Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102. Available at
  15. Hugo Herbelin & Stéphane Zimmermann (2009): An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. In: TLCA, pp. 142–156. Available at
  16. Delia Kesner & Stéphane Lengrand (2007): Resource operators for lambda-calculus. Inf. Comput. 205(4), pp. 419–473. Available at
  17. Olivier Laurent (1999): Polarized Proof-Nets: Proof-Nets for LC. In: TLCA, pp. 213–227. Available at
  18. Olivier Laurent (2002): Étude de la polarisation en logique. Thèse de doctorat. Université Aix-Marseille II.
  19. Olivier Laurent (2003): Polarized proof-nets and λμ-calculus. Theor. Comput. Sci. 290(1), pp. 161–188. Available at
  20. Ian Mackie (2005): Encoding Strategies in the Lambda Calculus with Interaction Nets. In: IFL, pp. 19–36. Available at
  21. John Maraist, Martin Odersky, David N. Turner & Philip Wadler (1999): Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus. Theor. Comput. Sci. 228(1-2), pp. 175–210. Available at
  22. Gordon D. Plotkin (1975): Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci. 1(2), pp. 125–159. Available at
  23. Alberto Pravato, Simona Ronchi Della Rocca & Luca Roversi (1999): The call-by-value λ-calculus: a semantic investigation. Math. Str. in Comput. Sci. 9(5), pp. 617–650. Available at
  24. Laurent Regnier (1992): Lambda-calcul et réseaux. PhD thesis. Univ. Paris VII.
  25. Amr Sabry & Matthias Felleisen (1993): Reasoning about Programs in Continuation-Passing Style. Lisp and Symbolic Computation 6(3-4), pp. 289–360. Available at
  26. Paolo Tranquilli (2009): Nets Between Determinism and Nondeterminism. Ph.D. thesis. Università degli Studi Roma Tre/Université Paris Diderot (Paris 7).
  27. Paolo Tranquilli (2011): Intuitionistic differential nets and lambda-calculus. Theor. Comput. Sci. 412(20), pp. 1979–1997. Available at
  28. Lionel Vaux (2007): λ-calcul différentiel et logique classique: interactions calculatoires. Ph.D. thesis. Université Aix-Marseille II.

Comments and questions to:
For website issues: