References

1

S. Abramsky.
The lazy $\lambda$-calculus.
In D. A. Turner, editor, Logical Foundations of Functional Programming, pages 65-116. Addison-Wesley, 1990.

2

W. Aitken.
A formal introduction to the lambda calculus.
Computer Science Dept., Cornell University, Ithaca, NY, 1993.

3

W. Aitken.
Metaprogramming in Nuprl Using Reflection.
PhD thesis, Computer Science Dept., Cornell University, Ithaca, NY, 1994.

4

W. Aitken and R. L. Constable.
Reflecting on Nuprl Lessons 1-4.
Technical report, Cornell University, Computer Science Dept., Ithaca, NY, 1992.
To appear.

5

W. Aitken, R. L. Constable, and J. Underwood.
Using reflected decision procedures.
Technical report, Department of Computer Science, Cornell University, Ithaca, NY, 1993.

6

S. F. Allen, R. L. Constable, D. J. Howe, and W. Aitken.
The semantics of reflected proof.
In Proceedings of the Fifth Symposium on Logic in Computer Science, pages 95-197. IEEE, June 1990.

7

G. S. Boolos and R. C. Jeffrey.
Computability and Logic, Second Edition.
Cambridge University Press, 1980.

8

R. S. Boyer and J. S. Moore.
Metafunctions: Proving them correct and using them efficiently as new proof procedures.
In The Correctness Problem in Computer Science, pages 103-84. Academic Press, New York, 1981.

9

J. Caldwell.
A constructive proof of propositional completeness in Nuprl.
Implementation notes, June 1993.

10

L. Cardelli and P. Longo.
A semantic basis for Quest.
In Journal of Functional Programming, pages 1:417-458, 1991.

11

T. Chan.
An algorithm for checking PL/CV arithmetic inferences.
In G. Goos and J. Hartmanis, editors, An Introduction to the PL/CV Programming Logic, Lecture Notes in Computer Science, Vol. 135, pages 227-264. Springer-Verlag, 1982.

12

R. L. Constable.
Assigning meaning to proofs: a semantic basis for problem solving environments.
Constructive Methods of Computing Science, NATO ASI Series, Vol. F55, pages 63-91, 1989.

13

R. L. Constable et al.
Implementing Mathematics with the Nuprl Development System.
Prentice-Hall, 1986.

14

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

15

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

16

M. Davis and J. T. Schwartz.
Metamathematical extensibility for theorem verifiers and proof checkers.
Comp. Mathematics with Applications, 5:217-230, 1979.

17

N. G. deBruijn.
A survey of the project Automath.
In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589-606. Academic Press, 1980.

18

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

19

S. Feferman.
Polymorphic typed lambda-calculi in a type faee axiomatic framework.
Contemporary Mathematics, 106:101-135, 1990.

20

S. Feferman.
Logics for termination and correctness of functional programs.
Technical report, Stanford University, Department of Mathematics, 1993.

21

J.-Y. Girard.
The system F of variable types: Fifteen years later.
Theoretical Computer Science, 45:159-192, 1986.

22

J.-Y. Girard.
Proof Theory and Logical Complexity, Volume 1.
Bibliopolis, Napoli, 1987.

23

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

24

M. Gordon and T. Melham.
Introduction to HOL: A Theorem Proving Environment for Higher-Oder Logic.
University Press, Cambridge, 1993.

25

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

26

S. Hayashi and H. Nakano.
PX: A Computational Logic.
MIT Press, Cambridge, MA, 1988.

27

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

28

D. J. Howe.
The computational behaviour of Girard's paradox.
In Proceedings of the Second Symposium on Logic in Computer Science, pages 205-214. IEEE, June 1987.

29

D. J. Howe.
Computational metatheory in Nuprl.
In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, Lecture Notes in Computer Science, Vol. 310, pages 238-257. Springer-Verlag, New York, 1988.

30

S. Igarashi, R. London, and D. Luckham.
Automatic program verification I: a logical basis and its implementation.
Acta Informatica, 4:145-82, 1975.

31

T. B. Knoblock and R. L. Constable.
Formalized metareasoning in type theory.
In Proceedings of the 1st Symposium on Logic in Computing Science, pages 237-248. IEEE, 1986.

32

D. Kozen.
Complexity of Finitely Presented Algebras.
PhD thesis, Computer Science Department, Cornell University, Ithaca, New York, 1977.

33

D. Kozen, M. Ben-Or, and J. Reif.
The complexity of elementary algebra and geometry.
In Proceedings of the 16th ACM Symposium on the Theory of Computing, pages 457-464, 1984.
Invited special issue Journal of Computer and System Sciences 32(2):251-264, 1985.

34

P. Martin-Löf.
An intuitionistic theory of types: Predicative part.
In Logic Colloquium '73, pages 73-118. North-Holland, Amsterdam, 1973.

35

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

36

D. A. McAllester.
ONTIC: A Knowledge Representation System for Mathematics.
MIT Press, Cambrige, Mass., 1989.

37

J. McCarthy.
A basis for a mathematical theory of computation.
In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33-70. Amsterdam:North-Holland, 1963.

38

D. Miller and G. Nadathur.
A logic programming approach to manipulating formulas and programs.
In IEEE Symposium on Logic Programming. ACM, 1987.

39

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

40

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

41

S. Owre, J. Rushby, and N. Shankar.
PVS: An integrated approach to specification and verification.
Preprint, January, 1992.

42

F. Pfenning.
Elf: a language for logic definition and verified metaprogramming.
In Proceedings of Fourth Symposium on Logic in Comp. Sci., pages 313-321, 1989.

43

G. D. Plotkin.
A structural approach to operational semantics.
Technical Report DAIMI-FN-19, Aarhus University, Aarhus University, Computer Science Dept., Denmark, 1981.

44

J. Rushby, F. von Henke, and S. Owre.
An introduction to formal specification and verification using EHDM.
Technical Report CSL-91-2, Computer Science Laboratory, SRI International, February, 1991.

45

B. Russell.
The Principles of Mathematics.
Cambridge University Press, Cambridge, 1908.

46

R. E. Shostak.
A practical decision procedure for arithmetic with function symbols.
Journal of the Association for Computing Machinery, 26:351-360, 1979.

47

B. Smith.
Reflection and semantics in Lisp.
Principles of Programming Languages, pages 23-35, 1984.

48

C. Smorynski.
Self-Reference and Modal Logic.
Springer-Verlag, NY, 1985.

49

A. Troelstra.
Metamathematical Investigation of Intuitionistic Mathematics, Lecture Notes in Mathematics, Vol. 344.
Springer-Verlag, 1973.

50

R. Weyrauch.
Prolegomena to a theory of formal reasoning.
Artificial Intelligence, 13:133-170, 1980.