1. Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: A transformation system for lazy functional logic programs. In: Middeldorp, A., Sato, T. (eds.) FLOPS 1999. LNCS, vol. 1722, pp. 147–162. Springer, Heidelberg (1999)

   Chapter  Google Scholar 

2. Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19, 20, 9–71 (1994)

   Article MathSciNet  Google Scholar 

3. Apt, K.R., Pedreschi, D.: Reasoning about termination of pure logic programs. Information and Computation 106, 109–157 (1993)

   Article MATH MathSciNet  Google Scholar 

4. Aravindan, C., Dung, P.M.: On the correctness of unfold/fold transformation of normal and extended logic programs. Journal of Logic Programming 24(3), 201–217 (1995)

   Article MATH MathSciNet  Google Scholar 

5. Basin, D., Deville, Y., Flener, P., Hamfelt, A., Fischer Nilsson, J.: Synthesis of programs in computational logic. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 30–65. Springer, Heidelberg (2004)

   Google Scholar 

6. Bossi, A., Cocco, N.: Basic transformation operations which preserve computed answer substitutions of logic programs. Journal of Logic Programming 16(1&2), 47–87 (1993)

   Article MATH MathSciNet  Google Scholar 

7. Bossi, A., Cocco, N.: Preserving universal termination through unfold/fold. In: Rodríguez-Artalejo, M., Levi, G. (eds.) ALP 1994. LNCS, vol. 850, pp. 269–286. Springer, Heidelberg (1994)

   Google Scholar 

8. Bossi, A., Cocco, N., Dulli, S.: A method for specializing logic programs. ACM Transactions on Programming Languages and Systems 12(2), 253–302 (1990)

   Article  Google Scholar 

9. Bossi, A., Cocco, N., Etalle, S.: Transforming normal programs by replacement. In: Pettorossi, A. (ed.) META 1992. LNCS, vol. 649, pp. 265–279. Springer, Heidelberg (1992)

   Google Scholar 

10. Bossi, A., Cocco, N., Etalle, S.: Simultaneous replacement in normal programs. Journal of Logic and Computation 6(1), 79–120 (1996)

    Article MATH MathSciNet  Google Scholar 

11. Bossi, A., Cocco, N., Etalle, S.: Transforming left-terminating programs: The reordering problem. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 33–45. Springer, Heidelberg (1996)

    Google Scholar 

12. Bossi, A., Etalle, S.: Transforming acyclic programs. ACM Transactions on Programming Languages and Systems 16(4), 1081–1096 (1994)

    Article  Google Scholar 

13. Bruynooghe, M., De Schreye, D., Krekels, B.: Compiling control. Journal of Logic Programming 6, 135–162 (1989)

    Article MATH  Google Scholar 

14. Bugliesi, M., Lamma, E., Mello, P.: Partial evaluation for hierarchies of logic theories. In: Debray, S., Hermenegildo, M. (eds.) Logic Programming: Proceedings of the 1990 North American Conference, Austin, Texas, October 1990, pp. 359–376. MIT Press, Cambridge (1990)

    Google Scholar 

15. Bugliesi, M., Rossi, F.: Partial evaluation in Prolog: Some Improvements about Cut. In: Lusk, E.L., Overbeek, R.A. (eds.) Logic Programming: Proceedings of the North American Conference 1989, Cleveland, Ohio, October 1989, pp. 645–660. MIT Press, Cambridge (1989)

    Google Scholar 

16. Bundy, A., Smaill, A., Wiggins, G.: The synthesis of logic programs from inductive proofs. In: Lloyd, J.W. (ed.) Computational Logic, Symposium Proceedings, Brussels, November 1990, pp. 135–149. Springer, Berlin (1990)

    Google Scholar 

17. Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)

    Article MATH MathSciNet  Google Scholar 

18. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

19. De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.H.: Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming 41(2–3), 231–277 (1999)

    Article MATH MathSciNet  Google Scholar 

20. Debray, S.K.: Optimizing almost-tail-recursive Prolog programs. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 204–219. Springer, Heidelberg (1985)

    Google Scholar 

21. Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3(3), 250–270 (2001)

    MATH  Google Scholar 

22. Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)

    Article MATH MathSciNet  Google Scholar 

23. Etalle, S., Gabbrielli, M., Marchiori, E.: A transformation system for CLP with dynamic scheduling and CCP. In: PEPM 1997, pp. 137–150. ACM Press, New York (1997)

    Chapter  Google Scholar 

24. Etalle, S., Gabbrielli, M., Meo, M.C.: Transformations of ccp programs. ACM Transactions on Programming Languages and Systems 23(3), 304–395 (2001)

    Article  Google Scholar 

25. Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL 2001, Florence (Italy), Technical Report DSSE-TR-2001-3, pp. 85–96. University of Southampton, UK (2001)

    Google Scholar 

26. Fioravanti, F., Pettorossi, A., Proietti, M.: Transformation rules for locally stratified constraint logic programs. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 292–340. Springer, Heidelberg (2004)

    Google Scholar 

27. Flener, P., Lau, K.-K., Ornaghi, M., Richardson, J.: An abstract formalization of correct schemas for program synthesis. Journal of Symbolic Computation 30(1), 93–127 (2000)

    Article MATH MathSciNet  Google Scholar 

28. Gallagher, J.P.: Transforming programs by specialising interpreters. In: Proceedings Seventh European Conference on Artificial Intelligence, ECAI 1986, pp. 109–122 (1986)

    Google Scholar 

29. Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Proceedings of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM 1993, Copenhagen, Denmark, pp. 88–98. ACM Press, New York (1993)

    Chapter  Google Scholar 

30. Gardner, P.A., Shepherdson, J.C.: Unfold/fold transformations of logic programs. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, pp. 565–583. MIT, Cambridge (1991)

    Google Scholar 

31. Hogger, C.J.: Derivation of logic programs. Journal of the ACM 28(2), 372–392 (1981)

    Article MATH MathSciNet  Google Scholar 

32. Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)

    MATH  Google Scholar 

33. Komorowski, H.J.: Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of Prolog. In: Ninth ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, pp. 255–267 (1982)

    Google Scholar 

34. Kott, L.: The McCarthy’s induction principle: ‘oldy’ but ‘goody’. Calcolo 19(1), 59–69 (1982)

    Article MATH MathSciNet  Google Scholar 

35. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM 17(8), 453–455 (1974)

    Article MATH MathSciNet  Google Scholar 

36. Lau, K.-K., Ornaghi, M., Pettorossi, A., Proietti, M.: Correctness of logic program transformation based on existential termination. In: Lloyd, J.W. (ed.) Proceedings of the 1995 International Logic Programming Symposium (ILPS 1995), pp. 480–494. MIT Press, Cambridge (1995)

    Google Scholar 

37. Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2(4&5), 461–515 (2002)

    Article MATH MathSciNet  Google Scholar 

38. Levi, G., Sardu, G.: Partial evaluation of meta programs in a multiple worlds logic language. New Generation Computing 6(2&3), 227–248 (1988)

    Article MATH  Google Scholar 

39. Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)

    MATH  Google Scholar 

40. Maher, M.J.: A transformation system for deductive database modules with perfect model semantics. Theoretical Computer Science 110, 377–403 (1993)

    Article MATH MathSciNet  Google Scholar 

41. Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Toplas 2, 90–121 (1980)

    Article MATH  Google Scholar 

42. The MAP transformation system (1995–2010),http://www.iasi.cnr.it/~proietti/system.html

43. Pettorossi, A.: A powerful strategy for deriving efficient programs by transformation. In: ACM Symposium on Lisp and Functional Programming, pp. 273–281. ACM Press, New York (1984)

    Chapter  Google Scholar 

44. Pettorossi, A., Proietti, M.: Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming 41(2&3), 197–230 (1999)

    Article MATH MathSciNet  Google Scholar 

45. Pettorossi, A., Proietti, M.: Perfect model checking via unfold/fold transformations. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 613–628. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

46. Pettorossi, A., Proietti, M., Renault, S.: Derivation of efficient logic programs by specialization and reduction of nondeterminism. Higher-Order and Symbolic Computation 18(1-2), 121–210 (2005)

    Article MATH  Google Scholar 

47. Pettorossi, A., Proietti, M., Senni, V.: Proving properties of constraint logic programs by eliminating existential variables. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 179–195. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

48. Pettorossi, A., Proietti, M., Senni, V.: Automatic correctness proofs for logic program transformations. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 364–379. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

49. Proietti, M., Pettorossi, A.: Semantics preserving transformation rules for Prolog. In: 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM 1991, Yale University, New Haven, Connecticut, USA, pp. 274–284. ACM Press, New York (1991)

    Chapter  Google Scholar 

50. Proietti, M., Pettorossi, A.: Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142(1), 89–124 (1995)

    Article MATH MathSciNet  Google Scholar 

51. Rabin, M.O.: Decidable theories. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 595–629. North-Holland, Amsterdam (1977)

    Chapter  Google Scholar 

52. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal on Foundations of Computer Science 13(3), 387–403 (2002)

    Article MATH MathSciNet  Google Scholar 

53. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: An unfold/fold transformation framework for definite logic programs. ACM Transactions on Programming Languages and Systems 26, 264–509 (2004)

    Article  Google Scholar 

54. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of parameterized systems using logic program transformations. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

55. Safra, S., Shapiro, E.: Meta interpreters for real. In: Kugler, H.J. (ed.) Proceedings Information Processing 1986, pp. 271–278. North-Holland, Amsterdam (1986)

    Google Scholar 

56. Sato, T., Tamaki, H.: Transformational logic program synthesis. In: Proceedings of the International Conference on Fifth Generation Computer Systems, pp. 195–201. ICOT (1984)

    Google Scholar 

57. Seki, H.: A comparative study of the well-founded and the stable model semantics: Transformation’s viewpoint. In: Proceedings of the Workshop on Logic Programming and Non-monotonic Logic, pp. 115–123. Cornell University (1990)

    Google Scholar 

58. Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)

    Article MATH MathSciNet  Google Scholar 

59. Seki, H.: Unfold/fold transformation of general logic programs for well-founded semantics. Journal of Logic Programming 16(1&2), 5–23 (1993)

    Article MATH MathSciNet  Google Scholar 

60. Seki, H.: On inductive and coinductive proofs via unfold/fold transformations. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 82–96. Springer, Heidelberg (2009)

    Google Scholar 

61. Sterling, L., Beer, R.D.: Incremental flavour-mixing of meta-interpreters for expert system construction. In: Proceedings of 3rd International Symposium on Logic Programming, Salt Lake City, Utah, USA, pp. 20–27. IEEE Press, Los Alamitos (1986)

    Google Scholar 

62. Tacchella, P., Gabbrielli, M., Meo, M.C.: Unfolding in CHR. In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2007), pp. 179–186 (2007)

    Google Scholar 

63. Takeuchi, A., Furukawa, K.: Partial evaluation of Prolog programs and its application to meta-programming. In: Kugler, H.J. (ed.) Proceedings of Information Processing 1986, pp. 415–420. North-Holland, Amsterdam (1986)

    Google Scholar 

64. Tamaki, H., Sato, T.: Unfold/fold transformation of logic programs. In: Tärnlund, S.-Å. (ed.) Proceedings of the Second International Conference on Logic Programming (ICLP 1984), pp. 127–138. Uppsala University, Uppsala (1984)

    Google Scholar 

65. Toni, F., Kowalski, R.: An argumentation-theoretic approach to logic program transformation. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 61–75. Springer, Heidelberg (1996)

    Google Scholar 

66. Venken, R.: A Prolog meta-interpretation for partial evaluation and its application to source-to-source transformation and query optimization. In: O’Shea, T. (ed.) Proceedings of ECAI 1984, pp. 91–100. North-Holland, Amsterdam (1984)

    Google Scholar 

67. Wadler, P.L.: Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science 73, 231–248 (1990)

    Article MATH MathSciNet  Google Scholar 

68. Zhang, J., Grant, P.W.: An automatic difference-list transformation algorithm for Prolog. In: Proceedings 1988 European Conference on Artificial Intelligence, ECAI 1988, pp. 320–325. Pitman (1988)

    Google Scholar 

Download references