Numbers in the following list are not consecutive because they are the same as in the List of All Publications
1. Dissertation: The metamathematics of constructive theories of effective operations. Stanford, 1972.
2. The non-derivability in intuitionistic formal systems of theorems on the continuity of effective operations, Journal of Symbolic Logic 40 (1976) 321-346.
3. The unprovability in intuitionistic formal systems of the continuity of effective operations on the reals, Journal of Symbolic Logic 41 (1976) 18-24.
4. Derived rules of inference related to the continuity of effective operations, Journal of Symbolic Logic 41 (1976) 328-336.
5. Continuity and comprehension in intuitionistic formal systems, Pacific J. Math 68 (1977) 29-40.
6. Principles of continuous choice and continuity of functions in formal systems for constructive mathematics, Annals of Mathematical Logic 12 (1977) 249-322.
9. A type-free Gödel interpretation, Journal of Symbolic Logic {43} (1978) 213-227.
10. Some relations between classical and constructive mathematics, Journal of Symbolic Logic 43 (1978) 228-246.
12. Goodman's theorem and beyond, Pacific J. Math 84 (1979) 1-16.
13. Continuity in intuitionistic set theories, in : Boffa, M., van Dalen, D., and McAloon, K. (eds.), Logic Colloquium '78, pp. 1-53. North-Holland, Amsterdam, 1979.
14. Extensionality and choice in constructive mathematics, Pacific J. Math 88 (1980) 1-28.
16. Formalizing constructive mathematics: why and how?, in Richman, F. (ed.) Constructive Mathematics, Proceedings, New Mexico, 1980}, Lecture Notes in Mathematics 873, pp. 146-191, Springer, Berlin, 1981.
17. Problematic principles in constructive mathematics, in: van Dalen, D., Lascar, D., Smiley, J. (eds.), Logic Colloquium '80, pp. 11-55, North-Holland, Amsterdam, 1982.
18. Recursive models for constructive set theories, Annals of Math. Logic 23 (1982) 127-178.
21. (with A. Scedrov) Church's thesis, continuity, and set theory,Journal of Symbolic Logic 49 (1984) 630-643.
23. Foundations of Constructive Mathematics: Metamathematical Studies, Springer, Berlin/Heidelberg/New York, 1985.
24. Proving programs and programming proofs, in: Barcan, Marcus, Dorn, and Weingartner (eds.), Logic, Methodology, and Philosophy of Science VII, proceedings of the International Congress, Salzburg, 1983, pp. 51-81, North-Holland, Amsterdam (1986). This paper has been translated into French and Russian .
25. Some theories conservative over intuitionistic arithmetic, in:Sieg, W. (ed.) Logic and Computation, volume 106 in the series Contemporary Mathematics¸ American Mathematical Society, Providence, R.I. (1987).
26. Computerizing Mathematics: Logic and Computation, in: The Universal Turing Machine: A Half-Century Survey}, edited by Herken, R., Oxford University Press (1988). Second Edition, Springer-Verlag, Berlin/ Heidelberg/ New York (1994)
27. Towards a computation system based on set theory, Theoretical Computer Science 60 (1988) 297-340.
35. Constructivism in the Nineties, in: Czermak, J. (ed.), Proceedings of the International Wittgenstein Symposium on Philosophy of Mathematics, Aug. 16-22, 1992. Wittgenstein Society, Vienna (1993).
const92.ps (1 mb, 15 pp.)
const92.ps.gz (300 kb)
const92.pdf (442 kb)
36. Using nonstandard analysis to verify the correctness of computations, International Journal of Foundations of Computer Science, Vol. 6, No. 3 (1995) 299-338.
dvi (156 kb, 40 pp.)
ps (3.2 mb, 40 pp.)
ps.gz (663 kb)
41. Reality and Truth in Mathematics, Philosophia Mathematica,1998.
ps (153 kb, 38 pp.)
ps (2 mb, 38 pp.)
ps.gz (640 kb)
47. with Freek Wiedijk: The meaning of infinity in calculus and computer algebra systems, in: Calmet, J., et. al. (eds.), Artificial Intelligence, Automated Reasoning, and Symbolic Computation: Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 2002, Proceedings, pp. 246-248, Lecture Notes in Artificial Intelligence 2385, Springer (2002).
See paper 52 below for an expanded version.
50. Lambda Logic, in Basin, David; Rusinowitch, Michael (eds.) Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings. Lecture Notes in Artificial Intelligence 3097, pp. 460-474, Springer (2004).
dvi(62 kb, 15 pages)
pdf(131 kb, 15 pages)
This paper gives the theoretical basis for the prover Otter-lambda.
Two proofs were omitted from this paper to meet the 15-page length limit. Those proofs can be found here:
dvi(24 kb, 6 pages)
pdf (84 kb, 6 pages)
53. with Robert Veroff and Larry Wos: Double negation elimination in some propositional logics , submitted to Studia Logica in November, 2002. Accepted in October, 2004 for a special issue on Negation in Constructive Logic.
dvi (141 kb, 41 pages).
pdf(185 kb, 41 pages)
This is a paper about logic, published in a logic journal, which contains many computer-generated proofs.
54. Constructivity, computability, and the continuum. To appear in Sica, Giandomenico (ed.)Advanced Studies in Mathematical Logic, volume 2, Polimetrica, Milan (2005).
dvi(115 kb, 29 pages)
pdf(197 kb, 29 pages)
This is a paper about the philosophy of constructive mathematics, containing some metamathematics, some physics, some philosophy, some history, and some mathematics. It was first presented as an invited talk at the Association for Symbolic Logic's spring meeting at Stanford, March 2005.
55. Implicit typing in lambda logic, submitted to LPAR-12. That conference will be held in December, 2005.
dvi(71 kb, 16 pages)
pdf(126 kb, 16 pages)
This theoretical paper addresses the relationship between proofs in a typed logic and proofs in lambda logic such as are found by Otter-lambda.