References

1

K. R. Apt and D. Pedreschi. Reasoning about termination of pure PROLOG programs. Information and Computation, 106(1):109--157, 1993.

2

K.R. Apt. Program Verification and Prolog. In E. Boerger, editor, Specification and Validation methods for Programming languages and systems, pages 55--95. Oxford University Press, 1995.

3

K.R. Apt and E. Marchiori. Reasoning about Prolog Programs: from Modes through Types to Assertions. Formal Aspects of Computing, 6A:743--764, 1994.

4

K.R. Apt, E. Marchiori, and C. Palamidessi. A theory of first order built in's of Prolog. Applicable Algebra in Engineering, Communication and Computing (AAECC), 5(3/4):159--191, 1994.

5

K.R. Apt and E. R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 1991. Texts and Monographs in Computer Science.

6

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

7

R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979.

8

K.L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 293--322. Plenum Press, 1978.

9

K. L. Clark. Predicate logic as a computational formalism. Res. Report DOC 79/59, Imperial College, Dept. of Computing, London, 1979.

10

K. Clark and S-Å. Tärnlund. A first order theory of data and programs. In Information Processing '77, pages 939--944. North-Holland, 1977.

11

P. Deransart. Proof method of declarative properties of definite programs. Theoretical Computer Science, 118:99--116, 1993.

12

G. Ferrand and P. Deransart. Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs. Journal of Logic Programming, 17:265--278, 1993.

13

Y. Deville. Logic Programming: Systematic Program Development. Addison-Wesley, 1990.

14

E. W. Djikstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.

15

A. Di Pierro, M. Martelli, and C. Palamidessi. Negation As Instantiation. To appear in Information and Computation, 1994.

16

C.J. Hogger. Introduction to Logic Programming. Academic Press, 1985.

17

L. C. Paulson. Introduction to Isabelle. Technical Report Technical Report 280, Cambridge University Computer Laboratory, Cambridge, 1993.

18

L. C. Paulson. Isabelle's object-logics. Technical Report Technical Report 286, Cambridge University Computer Laboratory, Cambridge, 1993.

19

J. M. Jacquet. Conclog: a Methodological Approach to Concurrent Logic Programming. volume 556 of Lecture Notes in Computer Science, Heidelberg, 1991. Springer-Verlag.

20

J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages, pages 111--119. ACM, 1987.

21

T. Kanamori and H. Seki. Verification of Prolog Programs Using an Extension of Execution. In Proceedings of the International Conference on Logic Programming, pages 475--489, 1986.

22

R. Kowalski. unpublished notes. Imperial College, 1985.

23

J. M. Lever. Proving Program Properties by means of SLS-Resolution. In K. Furukawa, editor, Proc. Eighth Int'l Conf. on Logic Programming, pages 614--628. The MIT Press, Cambridge, Mass., 1991.

24

J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

25

G. Nadathur and D. Miller. A Higher-Order Logic Programming. In C. Hogger D. Gabbay and A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press. To appear.

26

G. Nadathur and D. Miller. An overview of Prolog. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth ICLP, pages 810--827. The MIT Press, 1988.

27

V. A. Saraswat and M. Rinard. Concurrent constraint programming. In Proc. Seventeenth Annual ACM Symp. on Principles of Programming Languages. ACM, 1990.

28

V. A. Saraswat, M. Rinard, and P. Panangadnen. Semantic foundation of concurrent constraint programming. In Proc. Eighteenth Annual ACM Symp. on Principles of Programming Languages. ACM, 1991.

29

S. Renault. Generalizing the extended execution for normal programs. In LOPSTR 94, Fourth Workshop on Logic Program Synthesis and Transformation, June 1994.