Linear Lambda Calculus and Deep Inference

  • Luca Roversi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


We introduce a deep inference logical system SBVr which extends SBV [6] with Rename, a self-dual atom-renaming operator. We prove that the cut free subsystem BVr of SBVr exists. We embed the terms of linear λ-calculus with explicit substitutions into formulas of SBVr. Our embedding recalls the one of full λ-calculus into π-calculus. The proof-search inside SBVr and BVr is complete with respect to the evaluation of linear λ-calculus with explicit substitutions. Instead, only soundness of proof-search in SBVr holds. Rename is crucial to let proof-search simulate the substitution of a linear λ-terms for a variable in the course of linear β-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, exactly like linear λ-calculus with explicit substitutions can do.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. JFP 1(4), 375–416 (1991)zbMATHGoogle Scholar
  2. 2.
    Blute, R.F., Guglielmi, A., Ivanov, I.T., Panangaden, P., Straßburger, L.: A Logical Basis for Quantum Evolution and Entanglement. Private CommunicationGoogle Scholar
  3. 3.
    Brünnler, K., McKinley, R.: An algorithmic interpretation of a deep inference system. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 482–496. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    Bruscoli, P.: A purely logical account of sequentiality in proof search. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 302–316. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. CUP (1989)Google Scholar
  6. 6.
    Guglielmi, A.: A system of interaction and structure. ToCL 8(1), 1–64 (2007)CrossRefGoogle Scholar
  7. 7.
    Guglielmi, A., Straßburger, L.: A system of interaction and structure V: The exponentials and splitting. To appear on MSCS (2009)Google Scholar
  8. 8.
    Honda, K., Yoshida, N.: On the Reduction-based Process Semantics. TCS (151), 437–486 (1995)Google Scholar
  9. 9.
    Kahramanoğulları, O.: System BV is NP-complete. APAL 152(1-3), 107–121 (2007)zbMATHGoogle Scholar
  10. 10.
    Mairson, H.G.: Linear lambda calculus and ptime-completeness. JFP 14(6), 623–633 (2004)zbMATHGoogle Scholar
  11. 11.
    Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  12. 12.
    Milner, R.: Functions as processes. MSCS 2(2), 119–141 (1992)zbMATHGoogle Scholar
  13. 13.
    Roversi, L.: Linear lambda calculus with explicit substitutions as proof-search in Deep Inference (November 2010),
  14. 14.
    Straßburger, L.: Some observations on the proof theory of second order propositional multiplicative linear logic. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 309–324. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Straßburger, L., Guglielmi, A.: A system of interaction and structure IV: The exponentials and decomposition. ToCL (2010) (in press)Google Scholar
  16. 16.
    Straßburger, L.: System NEL is undecidable. In: De Queiroz, R., Pimentel, E., Figueiredo, L. (eds.) WoLLIC 2003. ENTCS, vol. 84. Elsevier, Amsterdam (2003)Google Scholar
  17. 17.
    van Bakel, S., Vigliotti, M.G.: A logical interpretation of the λ-calculus into the π-calculus, preserving spine reduction and types. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 84–98. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Luca Roversi
    • 1
  1. 1.Dip. di InformaticaTorinoItaly

Personalised recommendations