References

  1. Samson Abramsky (1993): Computational Interpretations of Linear Logic. Theor. Comput. Sci. 111(1&2), pp. 3–57. Available at http://dx.doi.org/10.1016/0304-3975(93)90181-R.
  2. Beniamino Accattoli (2011): Jumping around the box: graphical and operational studies on λ-calculus and Linear Logic. PhD thesis. La Sapienza University of Rome.
  3. Beniamino Accattoli (2012): An Abstract Factorization Theorem for Explicit Substitutions. In: RTA, pp. 6–21. Available at http://dx.doi.org/10.4230/LIPIcs.RTA.2012.6.
  4. Beniamino Accattoli (2012): A linear analysis of call-by-value λ-calculus. Available at the address https://sites.google.com/site/beniaminoaccattoli/Accattoli-Alinearanalysisofcall-by-valuelambdacalculus.pdf?attredirects=0.
  5. Beniamino Accattoli (2012): Proof nets and the call-by-value λ-calculus. LSFA 2012. Available at the address https://sites.google.com/site/beniaminoaccattoli/Accattoli-Proofnetsandthecallbyvaluelambdacalculus.pdf?attredirects=0.
  6. Beniamino Accattoli (2012): Proof Pearl: Abella Formalization of λ-Calculus Cube Property. In: CPP, pp. 173–187. Available at http://dx.doi.org/10.1007/978-3-642-35308-6_15.
  7. Beniamino Accattoli & Stefano Guerrini (2009): Jumping Boxes. In: CSL, pp. 55–70. Available at http://dx.doi.org/10.1007/978-3-642-04027-6_7.
  8. Beniamino Accattoli & Delia Kesner (2010): The Structural λ-Calculus. In: CSL, pp. 381–395. Available at http://dx.doi.org/10.1007/978-3-642-15205-4_30.
  9. Beniamino Accattoli & Ugo Dal Lago (2012): On the Invariance of the Unitary Cost Model for Head Reduction. In: RTA, pp. 22–37. Available at http://dx.doi.org/10.4230/LIPIcs.RTA.2012.22.
  10. Beniamino Accattoli & Luca Paolini (2012): Call-by-Value Solvability, revisited. In: FLOPS, pp. 4–16. Available at http://dx.doi.org/10.1007/978-3-642-29822-6_4.
  11. Emmanuel Beffara (2006): A Concurrent Model for Linear Logic. Electr. Notes Theor. Comput. Sci. 155, pp. 147–168. Available at http://dx.doi.org/10.1016/j.entcs.2005.11.055.
  12. Gianluigi Bellin & Philip J. Scott (1994): On the pi-Calculus and Linear Logic. Theor. Comput. Sci. 135(1), pp. 11–65. Available at http://dx.doi.org/10.1016/0304-3975(94)00104-9.
  13. Gérard Boudol (1998): The π-Calculus in Direct Style. Higher-Order and Symbolic Computation 11(2), pp. 177–208. Available at http://dx.doi.org/10.1023/A:1010064516533.
  14. Gérard Boudol & Cosimo Laneve (1996): The Discriminating Power of Multiplicities in the Lambda-Calculus. Inf. Comput. 126(1), pp. 83–102. Available at http://dx.doi.org/10.1006/inco.1996.0037.
  15. Luís Caires & Frank Pfenning (2010): Session Types as Intuitionistic Linear Propositions. In: CONCUR, pp. 222–236. Available at http://dx.doi.org/10.1007/978-3-642-15375-4_16.
  16. Matteo Cimini, Claudio Sacerdoti Coen & Davide Sangiorgi (2010): Functions as Processes: Termination and the λμtilde07Eμ-Calculus. In: TGC, pp. 73–86. Available at http://dx.doi.org/10.1007/978-3-642-15640-3_5.
  17. Pierre Clairambault (2011): Estimation of the Length of Interactions in Arena Game Semantics. In: FOSSACS, pp. 335–349. Available at http://dx.doi.org/10.1007/978-3-642-19805-2_23.
  18. Vincent Danos, Hugo Herbelin & Laurent Regnier (1996): Game Semantics & Abstract Machines. In: LICS, pp. 394–405. Available at http://doi.ieeecomputersociety.org/10.1109/LICS.1996.561456.
  19. Vincent Danos & Laurent Regnier (1999): Reversible, Irreversible and Optimal lambda-Machines. Theor. Comput. Sci. 227(1-2), pp. 79–97. Available at http://dx.doi.org/10.1016/S0304-3975(99)00049-3.
  20. Vincent Danos & Laurent Regnier (2004): Head Linear Reduction. Technical Report.
  21. Henry DeYoung, Luís Caires, Frank Pfenning & Bernardo Toninho (2012): Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. In: CSL, pp. 228–242. Available at http://dx.doi.org/10.4230/LIPIcs.CSL.2012.228.
  22. Thomas Ehrhard (2012): Collapsing non-idempotent intersection types. In: CSL, pp. 259–273. Available at http://dx.doi.org/10.4230/LIPIcs.CSL.2012.259.
  23. Thomas Ehrhard & Olivier Laurent (2010): Interpreting a finitary pi-calculus in differential interaction nets. Inf. Comput. 208(6), pp. 606–633. Available at http://dx.doi.org/10.1016/j.ic.2009.06.005.
  24. Thomas Ehrhard & Laurent Regnier (2006): Böhm Trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms. In: CiE, pp. 186–197. Available at http://dx.doi.org/10.1007/11780342_20.
  25. Andrew Gacek (2008): The Abella Interactive Theorem Prover (System Description). In: IJCAR, pp. 154–161. Available at http://dx.doi.org/10.1007/978-3-540-71070-7_13.
  26. Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102. Available at http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  27. Kohei Honda & Olivier Laurent (2010): An exact correspondence between a typed pi-calculus and polarised proof-nets. Theor. Comput. Sci. 411(22-24), pp. 2223–2238. Available at http://dx.doi.org/10.1016/j.tcs.2010.01.028.
  28. 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 http://dx.doi.org/10.1016/S0304-3975(98)00358-2.
  29. Gianfranco Mascari & Marco Pedicini (1994): Head Linear Reduction and Pure Proof Net Extraction. Theor. Comput. Sci. 135(1), pp. 111–137. Available at http://dx.doi.org/10.1016/0304-3975(94)90263-1.
  30. Damiano Mazza (2003): Pi et Lambda. Une étude sur la traduction des lambda-termes dans le pi-calcul. Memoire de DEA (in french).
  31. Dale Miller (1992): The pi-Calculus as a Theory in Linear Logic: Preliminary Results. In: ELP, pp. 242–264. Available at http://dx.doi.org/10.1007/3-540-56454-3_13.
  32. Dale Miller & Alwen Tiu (2010): Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. Comput. Log. 11(2). Available at http://doi.acm.org/10.1145/1656242.1656248.
  33. Robin Milner (1992): Functions as Processes. Math. Str. in Comput. Sci. 2(2), pp. 119–141. Available at http://dx.doi.org/10.1017/S0960129500001407.
  34. Robin Milner (2007): Local Bigraphs and Confluence: Two Conjectures. Electr. Notes Theor. Comput. Sci. 175(3), pp. 65–73. Available at http://dx.doi.org/10.1016/j.entcs.2006.07.035.
  35. Gordon D. Plotkin (1975): Call-by-Name, Call-by-Value and the lambda-Calculus. Theor. Comput. Sci. 1(2), pp. 125–159. Available at http://dx.doi.org/10.1016/0304-3975(75)90017-1.
  36. Davide Sangiorgi (1994): The Lazy Lambda Calculus in a Concurrency Scenario. Inf. Comput. 111(1), pp. 120–153. Available at http://dx.doi.org/10.1006/inco.1994.1042.
  37. Davide Sangiorgi (1999): From lambda to pi; or, Rediscovering continuations. Math. Str. in Comput. Sci. 9(4), pp. 367–401. Available at http://dx.doi.org/10.1017/S0960129599002881.
  38. Davide Sangiorgi & David Walker (2001): The Pi-Calculus - a theory of mobile processes. Cambridge University Press.
  39. Bernardo Toninho, Luís Caires & Frank Pfenning (2012): Functions as Session-Typed Processes. In: FoSSaCS, pp. 346–360. Available at http://dx.doi.org/10.1007/978-3-642-28729-9_23.
  40. Vasco Thudichum Vasconcelos (2005): Lambda and pi calculi, CAM and SECD machines. J. Funct. Program. 15(1), pp. 101–127. Available at http://dx.doi.org/10.1017/S0956796804005386.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org