References

1

H. Abelson and G. J. Sussman. Structure and Interpretation of Computer Programs. MIT Press, Cambridge, MA, 1985.

2

R. Backhouse. Constructive type theory-an introduction. In M. Broy, editor, Constructive Methods in Computer Science, NATO ASI Series, Vol. F55: Computer &System Sciences, pages 6-92. Springer-Verlag, New York, 1989.

3

R. Backhouse, P. Chisholm, G. Malcolm, and E. Saaman. Do-it-yourself type theory (part I). Formal Aspects of Computing, 1:19-84, 1989.

4

H. P. Barendregt. The Lambda Calculus: Its Syntax and Symantics, (Studies in Logic, Volume 103). North-Holland, Amsterdam, 1981.

5

B. Bloom. Can LCF be topped? flat lattice models of typed -calculus. Information and Computation, 87:264-301, 1990.

6

L. Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8:147-172, 1987.

7

E. Clarke, S. German, and J. Halpern. Effective axiomatizations of Hoare logics. J. Assoc. Comput. Mach., 30:612-636, 1983.

8

R. L. Constable, S. Allen, H. Bromley, W. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, N. Mendler, P. Panangaden, J. Sasaki, and S. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986.

9

T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76:95-120, 1988.

10

R. A. De Millo, R. J. Lipton, and A. J. Perlis. Social processes and proofs of theoremes and programs. Communications of the ACM, 22:271-280, 1979.

11

D. P. Friedman, M. Wand, and C. T. Haynes. Essentials of Programming Languages. MIT Press, 1992.

12

J. Gallier. Logic for Computer Science, Foundations of Automatic Theorem Proving. Harper and Row, NY, 1986.

13

J. Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge Tracts in Computer Science, Vol. 7. Cambridge University Press, 1989.

14

D. Gries. The Science of Programming. Springer-Verlag, New York, 1981.

15

D. Gries and F. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, New York, 1993.

16

C. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing Series. MIT Press, 1992.

17

C. Gunter and D.S.Scott. Semantic domains. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 633-674. North-Holland, 1990.

18

C. A. Gunter and J. C. Mitchell, editors. Theoretical Aspects of Object-Oriented Programming, Types, Semantics and Language Design. Types, Semantics, and Language Design. MIT Press, Cambridge, MA, 1994.

19

C. Hoare. An axiom basis for computer prgramming. In Comm. Assoc. Comput. Mach., volume 12, no. 10, pages 576-580,583, 1969.

20

C. Hoare. Notes on data structuring. In Structured Programming. Academic Press, New York, 1972.

21

G. Kahn. Natural semantics. In G. V.-N. F. Brandenburg and M. Wirsing, editors, STACS '87, chapter LNCS 247, pages 22-39. Springer-Verlag, Berlin, 1987.

22

S. C. Kleene. Introduction to Metamathematics. D. Van Nostrand, Princeton, 1952.

23

B. Meyer. Object-oriented software construction. Prentice-Hall, 1988.

24

R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1991.

25

A. Nerode and R. Shore. Logic for Applications. Springer-Verlag, New York, 1994.

26

L. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, NY, 1987.

27

L. C. Paulson. Standard ML for the Working Programmer. Cambridge University Press, 1991.

28

C. Reade. Elements of Functional Programming. Addison-Wesley, Reading, MA, 1989.

29

T. Reps and T. Teitelbaum. The Synthesizer Generator Reference Manual. Springer-Verlag, New York, third edition, 1988.

30

J. Reynolds. The coherence of languages with intersection types. In T. Ito and A. Meyer, editors, Theoretical Aspects of Computer Software, Int. Conf. TACS '91, Lecture Notes in Computer Science, Vol. 526, pages 675-700. Springer-Verlag, Sendai, Japan, 1991.

31

D. Schmidt. The Structure of Typed Programming Languages. MIT Press, Cambridge, 1994.

32

S. A. Schmidt. Denotational Semantics. W. C. Brown, Dubuque, Iowa, 1986.

33

D. Scott. Data types as lattices. SIAM J. Comput., 5:522-87, 1976.

34

D. S. Scott. A type theoretical alternative to CUCH, ISWIM, OWHY. Unpublished manuscript, 1969.

35

R. D. Tennent. Semantical analysis of specification logic. Information and Computation, 85(2):135-162, 1990.

36

R. D. Tennent. Semantics of Programming Languages. Prentice-Hall International, London, 1991.

37

S. Thompson. Type Theory and Functional Programming. Addison-Wesley, 1991.

38

R. Turner. Constructive Foundations for Functional Languages. McGraw Hill, New York, 1991.

39

G. Winskel. Formal Semantics of Programming Languages. MIT Press, Cambridge, 1993.