References

1

Stuart F. Allen. A non-type-theoretic semantics for type-theoretic language. PhD thesis, Cornell University, 1987.

2

Y. Bertot, G. Kahn, and L. Théry. Proof by pointing. In Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, volume 789, pages 141-160, 1994.

3

E. Bishop. Foundations of Constructive Analysis. McGraw Hill, NY, 1967.

4

P. Borras, D. Clément, T. Despeyroux, J. Incerpi, G. Kahn, B. Lang, and V. Pascual. Centaur: the system. In Software Engineering Notes, volume 13(5). Third Symposium on Software Development Environments, 1988.

5

N. Bourbaki. Elements of Mathematics, Theory of Sets. Addison-Wesley, Reading, MA, 1968.

6

Robert L. Constable. Using reflection to explain and enhance type theory. In Helmut Schwichtenberg, editor, Proof and Computation, volume 139 of NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20-August 1, NATO Series F, pages 65-100. Springer, Berlin, 1994.

7

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.

8

Robert L. Constable. The Structure of Nuprl's Type Theory in Logic and Computation. NATO ASI Series. Springer Verlag, 1996.

9

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.

10

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

11

Y. Coscoy, G. Kahn, and L. Théry. Extracting text from proofs. In Typed Lambda Calculus and its Applications, volume 902 of Lecture Notes in Computer Science, pages 109-123, 1995.

12

N. G. deBruijn. Set theory with type restrictions. In V.T. Sos A. Jahnal, R. Rado, editor, Infinite and Finite Sets, pages 205-314. vol. I, Coll. Math. Soc. J. Bolyai 10, 1975.

13

Michael Gordon and T. Melham. Introduction to HOL: a theorem proving environment for higher-order logic. University Press, Cambridge, 1993.

14

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.

15

Jason J. Hickey. Objects and theories as very dependent types. In Proceedings of FOOL 3, July 1996.

16

Jason J. Hickey. Nuprl-light: An implementation framework for hgher-order logics. In 14th International Conference on Automated Deduction, 1997.

17

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

18

Douglas J. Howe. Importing mathematics from HOL into Nuprl. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125, of LNCS, pages 267-282. Springer-Verlag, Berlin, 1996.

19

Douglas J. Howe. Semantic foundations for embedding HOL in Nuprl. In Martin Wirsing and Maurice Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of LNCS, pages 85-101. Springer-Verlag, Berlin, 1996.

20

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

21

Miroslava Kaloper and Piotr Rudnicki. Minimization of finite state machines. Mizar User's Association, 1996.

22

Dexter Kozen. Automata and Computability. Springer, 1997.

23

C. Kreitz. Constructive automata theory implemented with the Nuprl proof development system. Technical Report 86-779, Cornell University, Ithaca, New York, September 1986.

24

L. Magnusson and B. Nordström. The ALF proof editor and its proof engine. In Springer-Verlag, editor, Types for Proofs and Programs, volume 806 of Lecture Notes in Computer Science, pages 213-237, 1994.

25

Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-75. North-Holland, Amsterdam, 1982.

26

Per Martin-Löf. Intuitionistic Type Theory, Studies in Proof Theory, Lecture Notes. Bibliopolis, Napoli, 1984.

27

Alexei Nogin. Improving the efficiency of Nuprl proofs. Moscow State University, unpublished, 1997.

28

B. Nordstrom, K. Petersson, and J. Smith. Programming in Martin-Löf's Type Theory. Oxford Sciences Publication, Oxford, 1990.

29

L. Paulson and T. Nipkow. Isabelle: a generic theorem prover. Lecture Notes in Computer Science, Vol. 825, 1994.

30

L. C. Paulson. Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, Vol. 78. Springer-Verlag, 1994.

31

Robert Pollack. The Theory of LEGO:A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, Dept. of Computer Science, JCMaxwell Bldg, Mayfield Rd, Edinburgh EH9 3JZ, April 1995.

32

M. O. Rabin and D. Scott. Finite automata and their decision problems. In IBM Journal of Research and Development, volume 3(2), pages 115-125, 1959.

33

D. Scott. Constructive validity. In D. Lacombe M. Laudelt, editor, Symposium on Automatic Demonstration, volume 5(3) of Lecture Notes in Mathematics, pages 237-275. Springer-Verlag, New York, 1970.

34

L. Théry, Y. Bertot, and G. Kahn. Real theorem provers deserve real user-interfaces. In Software Engineering Notes, volume 17(5), pages 120-129. 5th Symposium on Software Development Environments, 1992.

35

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