[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Proofs, concurrent objects and computations in a FILL framework

  • Formalisms
  • Conference paper
  • First Online:
Object-Based Parallel and Distributed Computation (OBPDC 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1107))

Abstract

There are several major approaches to model concurrent computations using logic. In this context, one aim can be to achieve different forms of programming as logic, object-oriented or concurrent ones in a same logical language. Linear logic seems to be well-suited to describe computations that are concurrent and based on state transitions. In this paper, we propose and analyze a framework based on Full Intuitionistic Linear Logic (FILL), logical fragment with potentialities for non-determinisms management, as foundation of concurrent object-oriented programming, following the two paradigms proof-search as computation and proofs as computations.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1–2):3–58, 1993.

    Google Scholar 

  2. V. Alexiev. Applications of Linear Logic to Computation: An Overview. Bulletin of the IGPL, 2(1):77–107, 1994.

    Google Scholar 

  3. J.M. Andreoli and R. Pareschi. Logic programming with sequent systems: A linear logic approach. In Int. Workshop on Extensions of Logic Programming, LNCS 475, pages 1–30, Tübingen, Germany, December 1989.

    Google Scholar 

  4. J.M. Andreoli and R. Pareschi. Linear objects: logical processes with built-in inheritance. In 7th Conference on Logic Programming, MIT Press, pages 495–510, Jerusalem, June 1990.

    Google Scholar 

  5. J.M. Andreoli, R. Pareschi, and M. Bourgois. Dynamic programming as multiagent programming. In ECOOP'91 — Workshop on Object-Based Concurrent Computing, LNCS 612, pages 163–176, Genova, July 1991. Springer-Verlag.

    Google Scholar 

  6. N. Benton, G. Bierman, V. de Paiva, and M. Hyland. A term calculus for intuitionistic linear logic. In Int. Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 75–90, Utrecht, The Netherlands, March 1993.

    Google Scholar 

  7. G. Delzanno and M. Martelli. Objects in forum. In International Logic Programming Symposium, ILPS'95, Portland, Oregon, December 1995.

    Google Scholar 

  8. D. Galmiche. Canonical proofs for linear logic programming frameworks. In Workshop on Proof-theoretical extensions of logic programming, Santa Margherita Ligure, Italy, June 1994.

    Google Scholar 

  9. D. Galmiche and E. Boudinet. Proof search for programming in intuitionistic linear logic. In CADE-12 Workshop on Proof search in type-theoretic languages, Nancy, France, June 1994.

    Google Scholar 

  10. D. Galmiche and G. Perrier. Foundations of proof search strategies design in linear logic. In Logic at St Petersburg '94, Symposium on Logical Foundations of Computer Science, LNCS 813, pages 101–113, St Petersburg, Russia, July 1994.

    Google Scholar 

  11. D. Galmiche and G. Perrier. On proof normalization in linear logic. Theoretical Computer Science, 135(1):67–110, 1994.

    Google Scholar 

  12. J.Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

    Google Scholar 

  13. J. Harland and D. Pym. On resolution in fragments of classical linear logic. In LPAR'92, International Conference on Logic Programming and Automated Reasoning, LNAI 624, Pages 30–41, St. Petersburg, Russia, July 1992.

    Google Scholar 

  14. J. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Journal of Information and Computation, 110:327–365, 1994.

    Google Scholar 

  15. K. Honda and M. Tokoro. On asynchronous communication semantics. In ECOOP'91 — Workshop on Object-Based Concurrent Computing, LNCS 612, pages 21–51, Genova, July 1991. Springer-Verlag.

    Google Scholar 

  16. M. Hyland and V. de Paiva. Full intuitionistic linear logic (extended abstract). Annals of Pure and Applied Logic, 64:273–291, 1993.

    Google Scholar 

  17. M. Kanovich. Petri nets, Horn programs, Linear logic and Vector games. In Int. Symposium on. Theoretical Aspects of Computer Software, TACS'94, LNCS 789, pages 642–666, Sendai, Japan, April 1994.

    Google Scholar 

  18. N. Kobayashi and A. Yonezawa. ACL — a concurrent linear logic programming paradigm. In Int. Symposium on Logic Programming, pages 279–294, Vancouver, October 1993.

    Google Scholar 

  19. N. Kobayashi and A. Yonezawa. Asynchronous communication model based on linear logic. Formal Aspects of Computing, 3:279–294, 1994.

    Google Scholar 

  20. N. Kobayashi and A. Yonezawa. Higher-order concurrent linear logic programming. In Int. Workshop on Theory and Practice of Parallel Programming, LNCS 907, pages 137–166, Sendai, Japan, November 1994.

    Google Scholar 

  21. N. Kobayashi and A. Yonezawa. Type-theoretic foundations for concurrent object-oriented programming. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA'94, pages 31–45, 1994.

    Google Scholar 

  22. J. Lilius. High-level nets and linear logic. In 13th Int. Conference on Applications and Theory of Petri Nets, LNCS 616, pages 310–327, Sheffield, UK, 1992.

    Google Scholar 

  23. P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In 7th IEEE Symposium on Logic in Computer Science, pages 235–246, Santa-Cruz, California, June 1992.

    Google Scholar 

  24. P. Lincoln and V. Saraswat. Higher order, linear concurrent constraint programming. Manuscript, July 1992.

    Google Scholar 

  25. J. Meseguer. A logical theory of concurrent objects. In OOPSLA-ECOOP '90, pages 101–115, Ottawa, October 1990. Sigplan Notices, (25), 10.

    Google Scholar 

  26. J. Meseguer. Rewriting as a unified model of concurrency. In CONCUR'90, LNCS 458, pages 384–400, Amsterdam, August 1990.

    Google Scholar 

  27. J. Meseguer and N. Marti-Oliet. From Petri nets to Linear Logic. Math. Struct. in Comp. Science, 1:69–101, 1991.

    Google Scholar 

  28. D. Miller. The π-calculus as a theory of linear logic: Preliminary results. In Workshop on Extensions of Logic Programming, LNCS 660, pages 242–265, 1992.

    Google Scholar 

  29. D. Miller. A multiple-conclusion meta-logic. In 9th IEEE Symposium on Logic in Computer Science, pages 272–281, Paris, France, July 1994.

    Google Scholar 

  30. R. Milner. Functions as processes. Math. Struct. in Comp. Science, 2(2):119–146, 1992.

    Google Scholar 

  31. G. Perrier. Concurrent Programming in Linear Logic. Technical Report 95-R-052, CRIN-CNRS, Nancy, March 1995.

    Google Scholar 

  32. G. Perrier. A model of concurrency based on linear logic. In Conference on Computer Science Logic, CSL'95, Paderborn, Germany, 1995.

    Google Scholar 

  33. D. Pym and J. Harland. A uniform proof-theoretic investigation of linear logic programming. Journal of Logic and Computation, 4(2):175–207, 1994.

    Google Scholar 

  34. C. Retoré. Pomset logic: a non-commutative extension of classical linear logic. In Conference on Computer Science Logic, CSL'95, Paderborn, Germany, September 1995.

    Google Scholar 

  35. V.A. Saraswat. Concurrent constraint programming. In 7th ACM Symposium on Principles of Programming Languages, pages 232–245, San Francisco, California, 1990.

    Google Scholar 

  36. P. Volpe. Concurrent logic programming as uniform linear proofs. In Algebraic and Logic Programming, ALP'94, LNCS 850, pages 133–149, Madrid, Spain, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN-CNRS & INRIA Lorraine, Campus Scientifique, B.P. 239, 54506, Vandœuvre-lès-Nancy Cedex, France

    D. Galmiche & E. Boudinet

Authors
  1. D. Galmiche
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. E. Boudinet
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jean-Pierre Briot Jean-Marc Geib Akinori Yonezawa

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Galmiche, D., Boudinet, E. (1996). Proofs, concurrent objects and computations in a FILL framework. In: Briot, JP., Geib, JM., Yonezawa, A. (eds) Object-Based Parallel and Distributed Computation. OBPDC 1995. Lecture Notes in Computer Science, vol 1107. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61487-7_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-61487-7_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61487-6

  • Online ISBN: 978-3-540-68672-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation