References

1

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

2

A.V. Aho and J.D. Ullman. Foundations of Computer Science. Computer Science Press, New York, 1992.

3

J. R. Anderson, F. S. Bellezza, and C. F. Boyle. The geometry tutor and skill acquisition. In J. R. Anderson, editor, Rules of the Mind, chapter 8. Erlbaum, Hillsdale, New Jersey, 1993.

4

J. R. Anderson, C. F. Boyle, R. Farrell, and B. J. Reiser. Cognitive principles in the design of computer tutors. In P. Morris, editor, Modeling Cognition. Wiley, 1987.

5

J. R. Anderson, C. F. Boyle, and G. Yost. The geometry tutor. The Journal of Mathematical Behavior, 5(20), 1986.

6

John Barwise and John Etchemendy. The Language of First-Order Logic. Lecture Notes Number 23. Center for the Study of Language and Information, Stanford University, second edition, 1991.

7

John Barwise and John Etchemendy. Hyperproof. Center for the Study of Language and Information, Stanford University, Stanford, California, 1994.

8

J. L. Bates. A Logic for Correct Program Development. PhD thesis, Cornell University, 1979.

9

J. L. Bates and Robert L. Constable. Proofs as programs. ACM Trans. Program. Lang. and Syst., 7(1):53-71, 1985.

10

Nancy Baxter, Ed Dubinsky, and Gary Levin. Learning Discrete Mathematics with ISETL. Springer-Verlag, New York, 1989.

11

M. Beeson. The MathPert System, 1994. Personal Communication.

12

Albert H. Beiler. Recreations in the Theory of Numbers. Dover Publications Inc., New York, 1964.

13

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

14

J. S. Brown, A. Collins, and P. Duguid. Situated cognition and the culture of learning. Educational Researcher, 18(1):32-41, 1989.

15

J. S. Bruner. The Process of Education. Harvard University Press, Cambridge, Massachusetts, 1960.

16

A. Collins, J. S. Brown, and S. Newman. Cognitive apprenticeship: Teaching students the craft of reading, writing, and mathematics. In L. B. Resnick, editor, Knowing, Learning, and Instruction: Essays in Honor of Robert Glaser. Erlbaum, 1989.

17

J. Confrey. A theory of intellectual development. In For the Learning of Mathematics, volume 14(3), pages 2-8, 1994.

18

Jere Confrey. A review of the research on student conceptions in mathematics, science, and programming. In Courtney Cazden, editor, Review of Research in Education, chapter 1, pages 3-56. American Educational Research Association, 1990.

19

Robert L. Constable. Type theory as a foundation for computer science. In Theoretical Aspects of Computer Software, Int. Conf. TACS '91, Sendai, Japan, Lecture Notes in Computer Science, Vol. 526, pages 226-243, 1991.

20

Robert L. Constable. Experience using type theory as a foundation for computer science. In Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, pages 266-279. LICS, June 1995.

21

Robert L. Constable. Creating and evaluating interactive formal courseware for mathematics and computing. In Magdy F. Iskander, Mario J. Gonzalez, Gerald L. Engel, Craig K. Rushforth, Mark A. Yoder, Richard W. Grow, and Carl H. Durney, editors, Frontiers in Education, Salt Lake City, Utah, November 1996. IEEE.

22

Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986.

23

Robert L. Constable and Douglas J. Howe. Implementing metamathematics as an approach to automatic theorem proving. In R.B. Banerji, editor, Formal Techniques in Artificial Intelligence: A Source Book, pages 45-76. Elsevier Science Publishers (North-Holland), 1990.

24

Robert L. Constable, Paul B. Jackson, Pavel Naumov, and Juan Uribe. Constructively formalizing automata. In Proof Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge, 1997.

25

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

26

Antonella Cupillari. The Nuts and Bolts of Proofs. Wadsworth Publishing Co., Belmont, California, 1989.

27

James Davis and Daniel Huttenlocher. Shared annotations for cooperative learning. In Proceedings of the ACM Conference on Computer Supported Cooperative Learning, September 1995.

28

John Dewey. How We Think. Prometheus Books, Buffalo, New York, 1991.

29

R. Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. In The Journal of Symbolic Logic, pages Vol. 57, Number 3, September 1992.

30

Samuel Eilenberg. Automata, Languages and Machines, volume A. Academic Press, New York, 1974.

31

R. Gagné and L. J. Briggs. Principles of Instructional Design. Holt, Rinehart and Winston, New York, 1974.

32

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

33

D. R. Goldenson. Teaching introductory programming methods using structure editing: Some empirical results. In W. C. Ryan, editor, Proceedings of the National Educational Computing Conference 1989, pages 194-203, Eugene, Oregon, 1989. University of Oregon, International Council on Computers in Education.

34

Michael Gordon, Robin Milner, and Christopher Wadsworth. Edinburgh LCF: a mechanized logic of computation, Lecture Notes in Computer Science, Vol. 78. Springer-Verlag, NY, 1979.

35

N. Greenleaf. Bringing mathematics education into the algorithmic age. In Jr. J.P. Myers and M.J. O'Donnell, editors, Constructivity in Comupter Science, pages 199-217, New York, June 1991. Lecture Notes in Computer Science, Springer-Verlag.

36

David Gries and Fred B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, New York, 1993.

37

R. P. Grimaldi. Discrete and Combinatorial Mathematics: An Applied Introduction. Addison-Wesley, New York, 2nd edition, June 1989.

38

Hans Hahn. The crisis in intuition. In The World of Mathematics, pages 1956-1976. Simon &Schuster, New York, 1956.

39

Gila Hanna. Proofs that prove and proofs that explain. In G. Vergnaud, J. Rogalski, and M. Artigue, editors, Proceedings of the International Group for the Psychology of Mathematics Education, volume II, pages 45-51, Paris, 1989.

40

Gila Hanna. Challenges to the importance of proof. In For the Learning of mathematics, volume 15. FLM Publishing Association, Vancouver, British Columbia, Canada, November 1995.

41

D. Harel. Algorithmics: The Spirit of Computing. Addison-Wesley, Reading, MA, 1987.

42

Guershon Harel and Ed Dubinsky, editors. The Concept of Function, Aspects of Epistemology and Pedagogy, volume 25. Mathematical Association of America, 1992.

43

Leendert Helmink. Tools for Proofs and Programs. PhD thesis, Universiteit van Amsterdam, The Netherlands, 1992.

44

John E. Hopcroft and Jeffrey D. Ullman. Formal Languages and Their Relation to Automata. Addison-Wesley, Reading, Massachusetts, 1969.

45

Douglas J. Howe. Implementing number theory: An experiment with Nuprl. 8th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 230, pages 404-415, July 1987.

46

Paul B. Jackson. Exploring abstract algebra in constructive type theory. In A. Bundy, editor, CADE12, New York, June 1994. Springer-Verlag. LNAI.

47

Paul B. Jackson. Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. PhD thesis, Cornell University, Ithaca, NY, January 1995.

48

Paul B. Jackson. Developing a toolkit for floating-point hardware in the Nuprl proof development system. In Advanced Research Workshop on Correct Hardware Design Methodologies, pages 401-419, Organized by ESPRIT, Turin, Italy, June 1991.

49

L.S. Jutting. Checking Landau's `Grundlagen' in the AUTOMATH System. PhD thesis, Math Centre, Amsterdam, 1979.

50

Edward Kasner and James R. Newman. Paradox lost and paradox regained. In The World of Mathematics, pages 1936-1955. Simon &Schuster, 1956.

51

I. Lakatos. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press, Cambridge, MA, 1976.

52

C. L. Liu. Elements of Discrete Mathematics. McGraw-Hill, NY, 2nd edition, 1985.

53

Zhaohui Luo. Computation and Reasoning, A Type Theory for Computer Science. Oxford University Press, New York, 1994.

54

Wilbert J. McKeachie. Teaching Tips: Strategies, Research and Theory for College and University Teachers. D. C. Heath &Co., Toronto, 9th edition, 1994.

55

Kenneth R. Meyer and Dieter S. Schmidt, editors. Computer Aided Proofs in Analysis, volume 28 of The Institute for Mathematics and Its Applications. Springer-Verlag, New York, 1991.

56

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

57

A. Newell and H.A. Simon. Human Problem Solving. Prentice Hall, Englewood Cliffs, New Jersey, 1972.

58

James R. Newman. The World of Mathematics, volume 3. Simon &Schuster, New York, 1956.

59

O. Ore. Invitation to Number Theory. Mathematical Association of America, New York, 1967.

60

S. Owre, J.M. Rushby, and N. Shankar. PVS: A prototype verification system. In In Deepak Kapur, editor, Lecture Notes in Artificial Intelligence, pages 748-752, Saratoga, NY, 1992. 11th International Conference on Automated Deduction (CADE), Springer-Verlag. No. 607.

61

Erik Poll. A Programming Logic Based on Type Theory. PhD thesis, Technische Universiteit Eindhoven, 1994.

62

Stephen Read, editor. Computerised Logic Teaching Bulletin, volume Vol. ~2 No. 1. Bulletin of the Association for Computerised Logic Teaching, Scotland, March 1989.

63

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

64

Kenneth H. Rosen. Discrete Mathematics and Its Applications. McGraw-Hill, New York, 2nd edition, 1991.

65

R. Scheines and W. Sieg. An experimental comparison of alternative proof construction environments. Department of Philosophy CMU-PHIL-40, Carnegie Mellon University, Pittsburgh, Pennsylvania, August 1993.

66

Alan H. Schoenfeld. Mathematical Problem Solving. Academic Press, Inc., New York, 1985.

67

Herbert A. Simon. Problem solving and education. In D. Tuma and F. Reif, editors, Problem Solving and Education: Issues in Teaching and Research. Erlbaum, Hillsdale, New Jersey, 1980.

68

D. Sleeman and J. S. Brown, editors. Intelligent Tutoring Systems. Academic Press, London, 1982.

69

Daniel Solow. How to Read and Do Proofs: An Introduction to Mathematical Thought Process. John Wiley &Sons, New York, 1982.

70

E. Soloway and K. Ehrlich. Empirical studies of programming knowledge. IEEE Transactions on Software Engineering, SE-10(5):595-609, 1984.

71

Donald F. Stanat and David F. McAllister. Discrete Mathematics in Computer Science. Prentice-Hall, Englewood Cliffs, New Jersey, 1977.

72

Patrick Suppes. University-Level Computer-Assisted Instruction at Stanford: 1968-1980, volume IMSSS. Stanford University, Stanford, California, 1981.

73

David Tall, editor. Advanced Mathematicial Thinking. Kluwer Academic Publishers, 1991.

74

William P. Thurston. On proof and progress in mathematics. In For the Learning of Mathematics, volume 15. FLM Publishing Association, February 1995. Vancouver, British Columbia, Canada.

75

B. A. Trakhtenbrot. Algorithms and Automatic Computing Machines. D. C. Heath and Company, Lexington, Massachusetts, 1963.

76

A. Trybulec and P. Rudnicki. Using Mizar in computer aided instruction of mathematics. To appear, 1993.

77

Daniel J. Valleman. How to Prove It: A Structured Approach. Cambridge University Press, New York, 1994.

78

R. Wertheimer. The geometry proof tutor: An "intelligent" computer-based tutor in the classroom. Mathematics Teacher, pages 308-313, 1990.

79

A. N. Whitehead. The Aims of Education. MacMillan, New York, 1929.

80

A.N. Whitehead and B. Russell. Principia Mathematica, volume 1, 2, 3. Cambridge University Press, 2nd edition, 1925-27.

81

S. Wolfram. Mathematica: A System for Doing Mathematics by Computer. Addison-Wesley, 1988.