1. Alpuente, M., Sessa, M.I. (eds.): 1995 Joint Conference on Declarative Programming, GULP-PRODE 1995, Marina di Vietri, Italy (1995)

   Google Scholar 

2. Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)

   Article MATH MathSciNet  Google Scholar 

3. Andreoli, J.-M., Castagnetti, T., Pareschi, R.: Abstract interpretation of linear logic programming. In: Miller, D. (ed.) Proceedings of the International Logic Programming Symposium, Vancouver, Canada, pp. 295–314. MIT Press, Cambridge (1993)

   Google Scholar 

4. Andreoli, J.-M., Pareschi, R.: LO and behold! Concurrent structured processes. In: Proceedings of OOPSLA 1990, Ottawa, Canada, October 1990, vol. 25(10), pp. 44–56. Published as ACM SIGPLAN Notices (1990)

   Google Scholar 

5. Andreoli, J.-M., Pareschi, R.: Linear objects: Logical processes with built-in inheritance. New Generation Computing 9, 445–473 (1991)

   Article  Google Scholar 

6. Arcelli, F.: Aspetti di ordine superiore e di metalivello della programmazione logica. PhD thesis, DSI, Universitá di Milano (1991)

   Google Scholar 

7. Arcelli, F., Formato, F.: Implementing higher-order term-rewriting for program transformation inλProlog. In: Alpuente, Sessa [1], pp. 245–256

   Google Scholar 

8. Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 391–397. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

9. Baldoni, M., Giordano, L., Martelli, A.: A modal extension of logic programming: Modularity, beliefs and hypothetical reasoning. J. Log. Comput. 8(5), 597–635 (1998)

   Article MATH MathSciNet  Google Scholar 

10. Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: A transformational approach to negation in logic programming. Journal of Logic Programming 8, 201–228 (1990)

    Article MATH MathSciNet  Google Scholar 

11. Bossi, A., Meo, M.C.: Theoretical Foundations and Semantics. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, pp. 15–36. Springer, Heidelberg (2010)

    Google Scholar 

12. Bozzano, M., Delzanno, G., Martelli, M.: On the relations between disjunctive and linear logic programming. Electr. Notes Theor. Comput. Sci. 48 (2001)

    Google Scholar 

13. Bozzano, M., Delzanno, G., Martelli, M.: An effective fixpoint semantics for linear logic programs. Theory Pract. Log. Program. 2(1), 85–122 (2002)

    Article MATH MathSciNet  Google Scholar 

14. Bozzano, M., Delzanno, G., Martelli, M.: Model checking linear logic specifications. TPLP 4(5-6), 573–619 (2004)

    MATH MathSciNet  Google Scholar 

15. Bruscoli, P., Guglielmi, A.: Expressiveness of the abstract logic programming language Forum in planning and concurrency. In: Alpuente, M., Barbuti, R., Ramos, I. (eds.) GULP-PRODE (2), pp. 221–237 (1994)

    Google Scholar 

16. Bugliesi, M., Delzanno, G., Liquori, L., Martelli, M.: Object calculi in linear logic. J. Log. Comput. 10(1), 75–104 (2000)

    Article MATH MathSciNet  Google Scholar 

17. Bugliesi, M., Lamma, E., Mello, P.: Modularity in logic programming. J. Log. Program. 19/20, 443–502 (1994)

    Google Scholar 

18. Cervesato, I.: Petri nets and linear logic: a case study for logic programming. In: Alpuente, Sessa [1], pp. 313–320

    Google Scholar 

19. Cervesato, I.: Proof-theoretic foundation of compilation in logic programming languages. In: Jaffar, J. (ed.) Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (JICSLP 1998), Manchester, UK, pp. 115–129. MIT Press, Cambridge (1998)

    Google Scholar 

20. Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS (LNAI), vol. 1050, pp. 67–81. Springer, Heidelberg (1996)

    Google Scholar 

21. Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theoretical Computer Science 232(1-2), 133–163 (2000); Extended version of [20]

    Article MATH MathSciNet  Google Scholar 

22. Cervesato, I., Pfenning, F.: Linear higher-order pre-unification. In: Winskel, G. (ed.) Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS 1997), Warsaw, Poland, pp. 422–433. IEEE Computer Society Press, Los Alamitos (1997)

    Chapter  Google Scholar 

23. Cervesato, I., Pfenning, F.: A linear logical framework. Information and Computation (1998); Special issue with invited papers from LICS 1996, Clarke, E. (ed.)

    Google Scholar 

24. Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput. 13(5), 639–688 (2003)

    Article MATH MathSciNet  Google Scholar 

25. Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reasoning 40(2-3), 133–177 (2008)

    Article MATH MathSciNet  Google Scholar 

26. Chirimar, J.L.: Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania (May 1995)

    Google Scholar 

27. Costantini, S., Lanzarone, G.A.: A metalogic programming language. In: ICLP, pp. 218–233 (1989)

    Google Scholar 

28. Delzanno, G.: Logic and Object-Oriented Programming in Linear Logic. PhD thesis, Universitá di Pisa (February 1997)

    Google Scholar 

29. Delzanno, G., Giacobazzi, R., Ranzato, F.: Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) Programming. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, vol. 6125, pp. 136–158. Springer, Heidelberg (2010)

    Google Scholar 

30. Delzanno, G., Martelli, M.: Proofs as computations in linear logic. Theoretical Computer Science 258(1-2), 269–297 (2001)

    Article MATH MathSciNet  Google Scholar 

31. Dovier, A., Pontelli, E. (eds.): 25 Years of Logic Programming in Italy. LNCS, vol. 6125. Springer, Heidelberg (2010)

    Google Scholar 

32. Felty, A.P.: Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reasoning 11(1), 41–81 (1993)

    Article MathSciNet  Google Scholar 

33. Gabbay, D.M.: N-Prolog: An extension of Prolog with hypothetical implication II - logical foundations, and negation as failure. J. Log. Program. 2(4), 251–283 (1985)

    Article MATH MathSciNet  Google Scholar 

34. Gabbay, D.M., Reyle, U.: N-Prolog: An extension of Prolog with hypothetical implications I. J. Log. Program. 1(4), 319–355 (1984)

    Article MATH MathSciNet  Google Scholar 

35. Gabbrielli, M., Palamidessi, C., Valencia, F.D.: Concurrent and Reactive Constraint Programming. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, vol. 6125, pp. 231–253. Springer, Heidelberg (2010)

    Google Scholar 

36. Gacek, A.: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

37. Giordano, L., Olivetti, N.: Combining negation as failure and embedded implications in logic programs. J. Log. Program. 36(2), 91–147 (1998)

    Article MATH MathSciNet  Google Scholar 

38. Guglielmi, A.: Abstract Logic Programming in Linear Logic Independence and Causality in a First Order Calculus. PhD thesis, Universitá di Pisa (April 1996)

    Google Scholar 

39. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    MATH MathSciNet  Google Scholar 

40. Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4-5), 613–673 (2007)

    Article MATH MathSciNet  Google Scholar 

41. Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation 110(2), 327–365 (1994); A preliminary version appeared in the Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 32–42, Amsterdam, The Netherlands (July 1991)

    Google Scholar 

42. Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46) (2009)

    Google Scholar 

43. López, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Barahona, P., Felty, A.P. (eds.) PPDP, pp. 35–46. ACM, New York (2005)

    Google Scholar 

44. Miller, D.: Lexical scoping as universal quantification. In: Levi, G., Martelli, M. (eds.) Proceedings of the Sixth International Conference on Logic Programming, Lisbon, Portugal, pp. 268–283. MIT Press, Cambridge (1989)

    Google Scholar 

45. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS (LNAI), vol. 475, pp. 253–281. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

46. Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming 6(1-2), 79–108 (1989)

    Article MATH MathSciNet  Google Scholar 

47. Miller, D.: Abstractions in logic programming. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 329–359. Academic Press, London (1990)

    Google Scholar 

48. Miller, D.: A proposal for modules inλProlog. In: Dyckhoff, R. (ed.) ELP 1993. LNCS (LNAI), vol. 798. Springer, Heidelberg (1994)

    Google Scholar 

49. Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165(1), 201–232 (1996)

    Article MATH MathSciNet  Google Scholar 

50. Miller, D.: Overview of linear logic programming. In: Ehrhard, T., Girard, J.-Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science. London Mathematical Society Lecture Note, vol. 316, pp. 119–150. Cambridge University Press, Cambridge (2004)

    Chapter  Google Scholar 

51. Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic 51, 125–157 (1991)

    Article MATH MathSciNet  Google Scholar 

52. Momigliano, A.: Minimal negation and Hereditary Harrop Formulae. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol. 620, pp. 326–335. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

53. Momigliano, A.: Elimination of negation in a logical framework. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 411–426. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

54. Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher-order abstract syntax. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 375–391. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

55. Momigliano, A., Tiu, A.F.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 293–308. Springer, Heidelberg (2004)

    Google Scholar 

56. Nadathur, G.: Correspondences between classical, intuitionistic and uniform provability. Theoretical Computer Science 232, 273–298 (2000)

    Article MATH MathSciNet  Google Scholar 

57. Nadathur, G.: The metalanguageλProlog and its implementation. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol. 2024, pp. 1–20. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

58. Pareschi, R.: Type-Driven Natural Language Analysis. PhD thesis, University of Edinburgh. University of Pennsylvania, Department of Computer and Information Science, Technical Report No. MS-CIS-89-45 (July 1989)

    Google Scholar 

59. Pfenning, F.: Computation and deduction. Unpublished lecture notes, p. 217 (Revised March 2001) (May 1992)

    Google Scholar 

60. Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam (1999)

    Google Scholar 

61. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1988, pp. 199–208 (1988)

    Google Scholar 

62. Pfenning, F., Schürmann, C.: System description: Twelf — A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

63. Schürmann, C.: Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, CMU-CS-00-146 (2000)

    Google Scholar 

64. Warren, O.H.D.: Higher-order extensions to Prolog: Are they needed? In: Hayes, J.E., Michie, D., Pao, Y.-H. (eds.) Machine Intelligence, vol. 10, pp. 441–454. Halsted Press (1982)

    Google Scholar 

65. Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: The propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 355–377. Springer, Heidelberg (2004)

    Google Scholar 

66. Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: Specifying properties of concurrent computations in CLF. Electr. Notes Theor. Comput. Sci. 199, 67–87 (2008)

    Article MathSciNet  Google Scholar 

Download references