Monadic concurrent linear logic programming

ABSTRACT

Lolli is a logic programming language based on the asynchronous propositions of intuitionistic linear logic. It uses a backward chaining, backtracking operational semantics. In this paper we extend Lolli with the remaining connectives of intuitionistic linear logic restricted to occur inside a monad, an idea taken from the concurrent logical framework (CLF). The resulting language, called LolliMon, has a natural forward chaining, committed choice operational semantics inside the monad, while retaining Lolli's semantics outside the monad. LolliMon thereby cleanly integrates both concurrency and saturation with logic programming search. We illustrate its expressive power through several examples including an implementation of the pi-calculus, a call-by-need lambda-calculus, and several saturating algorithms presented in logical form.

REFERENCES

• 1: J.-M. Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):297--347, 1992.
• 2: Jean-Marc Andreoli , Remo Pareschi, LO and behold! Concurrent structured processes, Proceedings of the European conference on object-oriented programming on Object-oriented programming systems, languages, and applications, p.44-56, September 1990, Ottawa, Canada
• 3: Y. Bekkers and P. Tarau. Monadic constructs for logic programming. In J.Lloyd, editor, Proceedings of the International Symposium on Logic Programming (ILPS'95), pages 51--65, Portland, Oregon, Dec. 1995. MIT Press.
• 4: Marco Bozzano , Giorgio Delzanno , Maurizio Martelli, Model checking linear logic specifications, Theory and Practice of Logic Programming, v.4 n.5-6, p.573-619, September 2004 [doi>10.1017/S1471068404002066]
• 5: I. Cervesato, F. Pfenning, D. Walker, and K. Watkins. A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003.
• 6: Matt Fairtlough , Michael Mendler, Propositional lax logic, Information and Computation, v.137 n.1, p.1-33, Aug. 25, 1997 [doi>10.1006/inco.1997.2627]
• 7: T. Frühwirth. Theory and practice of constraint handling rules. Journal of Logic Programming, 37(1--3):95--138, Oct. 1998. Special Issue on Constraint Logic Programming.
• 8: Harald Ganzinger , David A. McAllester, A New Meta-complexity Theorem for Bottom-Up Logic Programs, Proceedings of the First International Joint Conference on Automated Reasoning, p.514-528, June 18-23, 2001
• 9: Harald Ganzinger , David A. McAllester, Logical Algorithms, Proceedings of the 18th International Conference on Logic Programming, p.209-223, July 29-August 01, 2002
• 10: Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
• 11: Robert H. Halstead, Jr., MULTILISP: a language for concurrent symbolic computation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.4, p.501-538, Oct. 1985 [doi>10.1145/4472.4478]
• 12: J. Harland, D. Pym, and M. Winikoff. Forward and backward chaining in linear logic. In D. Galmiche, editor, Proceedings of the Workshop on Type-Theoretic Languages: Proof Search and Semantics, volume 37 of Electronic Notes in Theoretical Computer Science, Pittsburgh, Pennsylvania, June 2000. Elsevier Science.
• 13: Joshua S. Hodas , Dale Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation, v.110 n.2, p.327-365, May 1, 1994
• 14: N. Kobayashi and A. Yonezawa. Typed higher-order concurrent linear logic programming. Technical Report 94-12, Department of Information Science, University of Tokyo, July 1994.
• 15: P. López and J. Polakow. Implementing efficient resource management for linear logic programming. In F. Baader and A. Voronkov, editors, Eleventh International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'04), pages 528--543, Montevideo, Uruguay, Mar. 2005. Springer-Verlag LNAI 3452.
• 16: David McAllester, On the complexity analysis of static analyses, Journal of the ACM (JACM), v.49 n.4, p.512-537, July 2002 [doi>10.1145/581771.581774]
• 17: R. McGrail. Monads and Control in Logic Programming. PhD thesis, Wesleyan University, 1997.
• 18: D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497--536, 1991.
• 19: Dale Miller, Forum: a multiple-conclusion specification logic, Theoretical Computer Science, v.165 n.1, p.201-232, Sept. 30, 1996
• 20: Dale A Miller , Gopalan Nadathur, Higher-order logic programming, Proceedings on Third international conference on logic programming, p.448-462, September 1986, London, United Kingdom
• 21: 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.
• 22: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 23: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 24: F. Pfenning. Substructural operational semantics and linear destination-passing style. In W.-N. Chin, editor, Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04), page 196, Taipei, Taiwan, Nov. 2004. Springer-Verlag LNCS 3302.
• 25: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 26: D. Pym and J. Harland. A uniform proof-theoretic investigation of linear logic programming. Journal of Logic and Computation, 4(2):175--207, April 1994.
• 27: R. Sekar , I. V. Ramakrishnan , Andrei Voronkov, Term indexing, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 28: Ehud Shapiro, The family of concurrent logic programming languages, ACM Computing Surveys (CSUR), v.21 n.3, p.413-510, Sep. 1989 [doi>10.1145/72551.72555]
• 29: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 30: K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003.
• 31: K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework: The propositional fragment. In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs, pages 355--377. Springer-Verlag LNCS 3085, 2004. Revised selected papers from the Third International Workshop on Types for Proofs and Programs, Torino, Italy, April 2003.

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

General Terms:
Languages, Theory

Keywords:
committed choice concurrency, linear logic, operational semantics