Skip to main content
SpringerLink
Log in
Book cover

Proof and Computation pp 379–395Cite as

Linear Logic and Computation: A Survey

  • Conference paper

Part of the book series: NATO ASI Series ((NATO ASI F,volume 139))

Abstract

This is a survey of computational aspects of linear logic related to proof search.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111: 3–57, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  2. S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Accepted for publication in Journal of Symbolic Logic, 1994. Draft available using anonymous ftp from the host theory.Doc.Ic.Ac.Uk and the file theory /pap ers/Abramsky/gfc. Dvi.

    Google Scholar 

  3. J.-M. Andreoli and R. Pareschi. Logic programming with sequent systems: a linear logic approach. In Proc. Workshop on Extensions of Logic Programming, Tuebingen. Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, 1990.

    Google Scholar 

  4. J.-M. Andreoli and R. Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation Computing, 9, 1991.

    Google Scholar 

  5. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2 (3), 1992.

    Google Scholar 

  6. N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Linear lambda-calculus and categorical models revisited. In Computer Science Logic’92, Selected Papers, pages 61–84. Springer LNCS, vol. 702, 1993.

    Google Scholar 

  7. A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183–220, 1992. Special Volume dedicated to the memory of John Myhill.

    Article  MATH  MathSciNet  Google Scholar 

  8. S. Cerrito. A linear axiomatization of negation as failure. Journal of Logic Programming, 12: 1–24, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  9. J. Chirimar, C. Gunter, and J. Riecke. Linear ML. In Proc. ACM Symposium on Lisp and Functional Programming, San Francisco. ACM Press, June 1992.

    Google Scholar 

  10. J. Chirimar, C. Gunter, and J. Riecke. Reference counting as a computational interpretation of linear logic. Manuscript, 1993. Available by anonymous ftp from the machine research att com in the file dist riecke linear logic journal.Ps.

    Google Scholar 

  11. V. Danos, J.-B. Joinet, and H. Schellinx. LKQ and LKT: sequent calculi for second order logic based upon dual linear decomposition of classical implication. Manuscript, October 1993.

    Google Scholar 

  12. V. Danos and L. Regnier. Local and asynchronous beta reduction. In Proc. 8-th IEEE Symp. on Logic in Computer Science, Montreal, pages 296–306. IEEE Computer Society Press, Los Alami- tos, California, June 1993.

    Google Scholar 

  13. R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57: 795–807, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  14. J.-Y. Girard. Linear logic. Theoretical Computer Science, 50: 1–102, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  15. J.-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1: 255–296, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  16. J.-Y. Girard. On the unity of logic. Annals of Pure and Applied Logic, 59: 201–217, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  17. G. Gonthier, M. Abadi, and J.-J. Levy. The geometry of optimal lambda reduction. In Proc. 19-th Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico. ACM Press, New York, NY, January 1992.

    Google Scholar 

  18. G. Gonthier, M. Abadi, and J.-J. Levy. Linear logic without boxes. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 223–234. IEEE Com-puter Society Press, Los Alamitos, California, June 1992.

    Google Scholar 

  19. J.S. Hodas. Specifying filler-gap dependency parsers in a linear logic programming language. In K. Apt, editor, Proc. Joint International Conference and Symposium on Logic Programming, pages 622–636, 1992.

    Google Scholar 

  20. J.S. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. In Proc. 6-th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pages 32–42. IEEE Computer Society Press, Los Alamitos, California, July 1991. Full paper to appear in Information and Computation. Draft available using anonymous ftp from host ftp.Cis.Upenn.Edu and the file pub/pap ers/miller/ic92. Dvi. Z.

    Google Scholar 

  21. J. Hudelmaier. Bounds for Cut Elimination in Intuitionistic Propositional Logic. PhD thesis, Universität Tübingen, 1989.

    Google Scholar 

  22. M. Kanovich. Horn programming in linear logic is NP-complete. In Proc. 7-th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, pages 200–210. IEEE Computer Society Press, Los Alamitos, California, June 1992. Full paper to appear in Annals of Pure and Applied Logic.

    Google Scholar 

  23. P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56:239–311, 1992. Special Volume dedicated to the memory of John Myhill.

    Article  MATH  MathSciNet  Google Scholar 

  24. P. Lincoln and A. Scedrov. First order linear logic without modalities is NEXPTIME-hard. Accepted for publication in Theoretical Computer Science, 1994. Available by anonymous ftp from host ftp.Cis.Upenn.Edu and the file pub papers scedrov malll.Dvi.

    Google Scholar 

  25. P. Lincoln, A. Scedrov, and N. Shankar. Linearizing intuitionistic implication. Annals of Pure and Applied Logic, 60: 151–177, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  26. P. Lincoln and N. Shankar. Proof search in first order linear logic. Manuscript, October 1993.

    Google Scholar 

  27. P. Lincoln and T. Winkler. Constant-Only Multiplicative Linear Logic is NP-Complete. Manuscript, September 1992. Available using anonymous ftp from host ftp.Csl.Sri.Com and the file pub/lincoln/ comul t-np c. Dvi.

    Google Scholar 

  28. P.D.Lincoln. Computational A spects of Linear Logic. PhD thesis, Stanford University, 1992.

    Google Scholar 

  29. D. Miller. Abstractions in logic programming. In P. Odifreddi, editor, Logic and Computer Science, pages 329–359. APIC Studies in Data Processing, Vol. 31, Academic Press, 1990.

    Google Scholar 

  30. D. Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, Proceedings of the 1992 Workshop on Extensions to Logic Programming, number 660 in Lecture Notes in Computer Science, pages 242–265. Springer-Verlag, 1993. Available using anonymous ftp from host ftp.Cis.Upenn.Edu and the file pub/papers/miller/pic.Dvi.Z.

    Google Scholar 

  31. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991. Special Issue on the 2-nd Annual IEEE Symposium on Logic in Computer Science, 1987.

    Article  MathSciNet  Google Scholar 

  32. A. Scedrov. A brief guide to linear logic. In G. Rozenberg and A. Salomaa, editors, Current Trends in Theoretical Computer Science, pages 377–394. World Scientific Publishing Co., 1993.

    Google Scholar 

  33. N. Shankar. Proof search in the intuitionistic sequent calculus. In Proc. of the 11th International Conference on Automated Deduction, pages 522–536. Springer LNAI, vol. 607, 1992.

    Google Scholar 

  34. E.Y. Shapiro. Alternation and the computational complexity of logic programs. Journal of Logic Programming, 1: 19–33, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  35. L. Stockmeyer. Classifying the computational complexity of problems. Journal of Symbolic Logic, 52: 1–43, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  36. A.S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes No. 29. Center for the Study of Language and Information, Stanford University, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of Pennsylvania, Philadelphia, PA, 19104-6395, USA

    Andre Scedrov

Authors
  1. Andre Scedrov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematisches Institut, Ludwig-Maximilians-Universität München, Theresienstraße 39, D-80333, München, Germany

    Helmut Schwichtenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Scedrov, A. (1995). Linear Logic and Computation: A Survey. In: Schwichtenberg, H. (eds) Proof and Computation. NATO ASI Series, vol 139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-79361-5_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-79361-5_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-79363-9

  • Online ISBN: 978-3-642-79361-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation