Bibliography

1

Peter H. G. Aczel.
The type theoretic interpretation of constructive set theory.
In R. B. Marcus, G. J. W. Dorn, and P. Weingartner, editors, Logic, Methodology and Philosophy of Science VII, pages 17-49, Amsterdam, 1986. Elsevier Science Publishers.

2

Stuart F. Allen.
A non-type-theoretic definition of Martin-Löf's types.
In Proceedings of the Second Symposium on Logic in Computer Science, pages 215-224, Washington, D.C., 1987. IEEE Computer Society.

3

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

4

Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken.
The semantics of reflected proof.
In Proceedings of the Fifth Symposium on Logic in Computer Science, pages 95-197, Washington, D.C., 1990. IEEE Computer Society.

5

R. C. 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, Berlin, 1989.

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

D. Basin and Robert L. Constable.
Metalogical frameworks.
In G. Huet and G. Plotkin, editors, Logical Environments, chapter 1, pages 1-29. Cambridge University Press, 1993.

8

J. L. Bates and Robert L. Constable.
Proofs as programs.
ACM Transactions on Programming Languages and Systems, 7(1):53-71, 1985.

9

M. J. Beeson.
Foundations of Constructive Mathematics.
Springer-Verlag, Berlin, 1985.

10

John L. Bell.
Toposes and Local Set Theories.
Oxford Logic Guides #14. Oxford University Press, 1988.

11

Paul Bernays.
Axiomatic Set Theory.
North-Holland, Amsterdam, 1958.
With an introduction by A.A. FraenkelFraenkel, A. A.

12

E. Bishop.
Foundations of Constructive Analysis.
McGraw Hill, New York, 1967.

13

E. Bishop and D. Bridges.
Constructive Analysis.
Springer-Verlag, Berlin, 1985.

14

W. W. Bledsoe.
A new method for proving certain Presburger formulas.
In Proceedings of the Fourth International Joint Conference on Artificial Intelligence, held in Tbilisi, Georgia, USSR, 1975.

15

N. Bourbaki.
Elements of Mathematics, Algebra, Volume 1.
Addison-Wesley, Reading, Massachusetts, 1968.

16

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

17

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

18

R. S. Boyer and J. S. Moore.
Integrating recursive procedures into hueristic theorem provers: A case study in linear arithmetic.
In Machine Intelligence II. Oxford University Press, 1988.

19

L. E. J. Brouwer.
Collected Works, volume 1.
North-Holland, Amsterdam, 1975.
Edited by A. Heyting.

20

A. Bundy.
The use of proof plans for normalization.
In R. S. Boyer, editor, Essays in Honor of Woody BledsoeBledsoe, W. W., pages 149-166. Kluwer Academic Publishers, Dordrecht, Boston, 1991.

21

S. R. Buss.
The polynomial hierarchy and intuitionistic bounded arithmetic.
In A. L. Selman, editor, Structure in Complexity Theory, Lecture Notes in Computer Science #223, pages 77-103, Berlin, 1986. Springer-Verlag.

22

T. Chan.
An algorithm for checking PL/CV arithmetic inferences.
In R. L. Constable, S. D. Johnson, and C. D. Eichenlaub, editors, An Introduction to the PL/CV2 Programming Logic, Lecture Notes in Computer Science #135, pages 227-264. Springer-Verlag, Berlin, 1982.

23

L. Paul Chew, Robert L. Constable, Stephen Vavasis, Keshav Pingali, and Richard Zippel.
Collaborative mathematics environments.
www@cs.cornell.edu/Info/Projects/Nuprl, 1996.

24

Noam Chomsky.
Language and Problems of Knowledge: Manaqua Lectures.
MIT Press, Cambridge, Massachusetts, 1988.

25

Alonzo Church.
A formulation of the simple theory of types.
Journal of Symbolic Logic, 5:55-68, 1940.

26

Alonzo Church.
Introduction to Mathematical Logic, Vol I.
Princeton University Press, 1956.

27

Alonzo Church.
Application of recursive arithmetic to the problem of circuit synthesis,.
In Summaries of talks presented at the Summer Institute for Symbolic Logic, Cornell University 1957, pages 3-50, Princeton, 1960. Institute for Defense Analyses.

28

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

29

Robert L. Constable.
Constructive mathematics and automatic program writers.
In C. V. Freiman, J. E. Griffith, and J. L. Rosenfeld, editors, Proceedings of Information Processing 71 (IFIP), pages 229-233, Amsterdam, 1972. North-Holland.

30

Robert L. Constable.
Assigning meaning to proofs: a semantic basis for problem solving environments.
In M. Broy, editor, Constructive Methods in Computer Science, NATO ASI Series, Vol. F55: Computer & System Sciences, pages 63-91. Springer-Verlag, Berlin, 1989.

31

Robert L. Constable.
Type theory as a foundation for computer science.
In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS '91, Lecture Notes in Computer Science #526, pages 226-243, Berlin, 1991. Springer-Verlag.

32

Robert L. Constable, Paul B. Jackson, Pavel Naumov, and Juan Uribe.
Constructively formalizing automata theory I: Finite automata.
In Robin Milner Festschrift. Springer-Verlag, Berlin, 1998.
To appear.

33

Robert L. Constable, S. D. Johnson, and C. D. Eichenlaub.
Introduction to the PL/CV2 progamming logic.
In R. L. Constable, S. D. Johnson, and C. D. Eichenlaub, editors, An Introduction to the PL/CV2 Programming Logic, Lecture Notes in Computer Science #135, pages 165-178, Berlin, 1982. Springer-Verlag.

34

Robert L. Constable and N. P. Mendler.
Recursive Definitions in Type Theory.
In R. Parikh, editor, Logics of Programs, Lecture Notes in Computer Science #193, pages 61-78, Berlin, 1985. Springer-Verlag.

35

Robert L. Constable and Scott F. Smith.
Computational foundations of basic recursive function theory.
Theoretical Computer Science, 121:89-112, December 1993.

36

Thierry Coquand.
Metamathematical investigations of a calculus of constructions.
In P. Odifreddi, editor, Logic and Computer Science, pages 91-122. Academic Press, London, 1990.

37

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

38

Thierry Coquand and Christine Paulin-Mohring.
Inductively defined types, preliminary version.
In P. Martin-Löf and G. E. Mints, editors, COLOG '88, International Conference on Computer Logic, Lecture Notes in Computer Science #417, pages 50-66, Berlin, 1990. Springer-Verlag.

39

H. B. Curry and R. Feys.
Combinatory Logic, Volume I.
North-Holland, Amsterdam, 1958.

40

N. G. de Bruijn.
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, New York, 1980. Academic Press.

41

Peter Dybjer.
Inductive families.
Formal Aspects of Computing, 6:1-26, 1994.

42

William M. Farmer.
A partial functions version of Church's simple theory of types.
Journal of Symbolic Logic, 55(3):1269-1291, September 1990.

43

William M. Farmer, Joshua D. Guttman, and F. Javier Thayer.
IMPS: an interactive mathematical proof system.
Technical Report M90-19, The MITRE Corp., Bedford, Massachusetts, 1991.

44

Gottlob Frege.
Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens.
Halle, 1879.
English translation in [], pp.1-82.

45

Gottlob Frege.
Grundgesetze der Arithmetik, Begriffsschriftlich Abgeleitet.
Pohle, Jena, 1903.
Reprinted 1962, Olms, Hildesheim.

46

H. M. Friedman and A. Scedrov.
Set existence property for intuitionistic theories with countable choice.
Annals of Pure and Applied Logic, 25:129-140, 1983.

47

Gerhard Gentzen.
Untersuchungen über das logische Schliessen.
Mathematische Zeitschrift, 39:176-210, 405-431, 1935.
English translation in: [], pp.68-131.

48

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

49

J-Y. Girard.
A new constructive logic: classical logic.
Mathematical Structures in Computer Science, 1:255-296, 1991.

50

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

51

Kurt Gödel.
Über formal unentscheidbar Sätze der principa mathematica und verwandter Systeme i.
Monatshefte für Mathematik und Physik, 38:173-198, 1931.
Reprinted and translated in [, pp.144-195].

52

Kurt Gödel.
Zur intuitionistisched Arithmetic und Zahlentheorie.
Ergebnisse eines Mathematischen Kolloquiums, 4:34-38, 1933.
Reprinted and translated in [, pp.282-295].

53

D. Good.
Mechanical proofs about computer programs.
In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 55-75, Englewood Cliffs, New Jersey, 1985. Prentice-Hall.

54

Michael Gordon and T. Melham.
Introduction to HOL.
University Press, Cambridge, 1993.

55

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

56

T. G. Griffin.
Notational definition - a formal account.
In Proceedings of the Third Annual Symposium on Logic in Computer Science, pages 372-383, Los Alamitos, California, 1988. IEEE Computer Society.

57

T. G. Griffin.
Notational Definition and Top-Down Refinement for Interactive Proof Development Systems.
PhD thesis, Cornell University, 1988.

58

Juris Hartmanis and R. Stearns.
On the computational complexity of algorithms.
Transactions of the American Mathematics Society, 117:285-306, 1965.

59

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

60

Jason J. Hickey.
Formal abstract data types.
unpublished manuscript, 1996.

61

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

62

Jason J. Hickey.
Nuprl-Light: An implementation framework for higher-order logics.
In W. McCune, editor, CADE-14: 14th International Conference on Automated Deduction, Lecture Notes in Computer Science #1249, pages 395-399, Berlin, 1997. Springer-Verlag.

63

David Hilbert.
Über das Unendliche.
Mathematische Annalen, 95:161-190, 1926.

64

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

65

Paul B. Jackson.
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra.
PhD thesis, Cornell University, August 1994.
Forthcoming.

66

Paul B. Jackson.
The Nuprl Proof Development System, Version 4.1 Reference Manual and User's Guide.
Cornell University, Ithaca, New York, February 1994.

67

A. Joyal and Ieke Moerdijk.
Algebraic Set Theory.
Cambridge University Press, Cambridge, 1995.

68

G. Kreisel.
Interpretation of analysis by means of constructive functionals of finite type.
In A. Heyting, editor, Constructivity in Mathematics: Proceedings of the Colloquium held at Amsterdam, 1957, pages 101-128, Amsterdam, 1959. North-Holland.

69

G. Kreisel.
Neglected possibilities of processing assertions and proofs mechanically: choice of problems and data.
In P. Suppes, editor, University-Level Computer-Assisted Instruction at Stanford: 1968-1980, pages 131-147. Institute for Mathematical Studies in the Social Sciences, Stanford University, 1981.

70

Christoph Kreitz.
Program synthesis.
In W. Bibel and P. Schmitt, editors, Automated Deduction - A Basis for Applications, chapter III.2.10. Kluwer Academic Publishers, Dordrecht, Boston.
To appear.

71

S. Kripke.
Semantical analysis of intuitionistic logic I.
In J. N. Crossley and M. A. E. Dummett, editors, Formal Systems and Recursive Functions, pages 92-130. North-Holland, Amsterdam, 1965.

72

J. Lambek and P. J. Scott.
Introduction to Higher-Order Categorical Logic, volume 7 of Cambridge Studies in Advanced Mathematics.
Cambridge University Press, Cambridge, UK, 1986.

73

H. Läuchli.
An abstract notion of realizability for which intuitionistic predicate calculus is complete.
In A. Kino, J. Myhill, and R. E. Vesley, editors, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968, pages 227-34, Amsterdam, 1970. North-Holland.

74

Daniel Leivant.
A foundational delineation of poly-time.
Information and Computation, 110:391-420, 1994.

75

Daniel Leivant.
Predicative recurrence in finite type.
In A. Nerode and Yu. V. Matijacevic, editors, Logical Foundations of Computer Science, Lecture Notes in Computer Science #813, pages 227-239. Springer-Verlag, Berlin, 1994.

76

Daniel Leivant.
Ramified recurrence and computational complexity I: Word recurrence and polynomial time.
In P. Clote and J. B. Remmel, editors, Feasible Mathematics II, Perspectives in Computer Science. Birkhäuser, Boston, 1995.

77

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

78

Saunders MacLane and Ieke Moerdijk.
Sheaves in Geometry and Logic, a First Introduction to Topos Theory.
Springer-Verlag, Berlin, 1992.

79

A. A. Markov.
On the representation of recursive functions (Russian).
Izvestiya Akad. Nauk SSSR. Ser. Mat., 13:417-424, 1949.
English translation: American Mathematical Society Translation 54 (1950) 13 pp.

80

Per Martin-Löf.
Constructive mathematics and computer programming.
In L. Jonathan Cohen, J. os, H. Pfeiffer, and K.-P. Podewski, editors, Proceedings of the Sixth International Congress on Logic, Methodology, and Philosophy of Science, pages 153-75, Amsterdam, 1982. North-Holland.

81

Per Martin-Löf.
On the meaning of the logical constants and the justification of the logical laws.
Lectures in Siena, 1983.

82

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

83

D. A. McAllester.
ONTIC: A Knowledge Representation System for Mathematics.
MIT Press, Cambridge, Massachusetts, 1989.

84

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. North-Holland, Amsterdam, 1963.

85

J. McCarthy et al.
Lisp 1.5 Users Manual.
Mit Press, Cambridge, Massachusetts, 1962.

86

P. F. Mendler.
Inductive Definition in Type Theory.
PhD thesis, Cornell University, Ithaca, New York, 1988.

87

Ieke Moerdijk and Gonzalo E. Reyes.
Models for Smooth Infinitesimal Analysis.
Springer-Verlag, Berlin, 1991.

88

Chetan Murthy.
An evaluation semantics for classical proofs.
In Proceedings of the Sixth Symposium on Logic in Computer Science, pages 96-109, Los Alamitos, California, 1991. IEEE Computer Society.

89

B. Nordstrom, K. Petersson, and J. M. Smith.
Programming in Martin-Löf's Type Theory.
Clarendon Press, Oxford University Press, 1990.

90

John O'Leary, Miriam Leeser, Jason J. Hickey, and Mark Aagaard.
Non-restoring integer square root: A case study in design by principled optimization.
In T. Kropf and R. Kumar, editors, Theorem Provers in Circuit Design: Second International Conference (TPCD '94), Lecture Notes in Computer Science #901, pages 52-71, Berlin, 1995. Springer-Verlag.

91

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

92

Erik Palmgren.
On Fixed Point Operators, Inductive Definitions and Universes in Martin-Löf's Type Theory.
PhD thesis, Uppsala University, March 1991.

93

Erik Palmgren.
A sheaf-theoretic foundation for nonstandard analysis.
Technical Report 1995:43, Department of Mathematics, Uppsala University, 1995.

94

Christine Paulin-Mohring.
Extracting F_w's programs from proofs in the calculus of constructions.
In Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, pages 89-104, New York, 1989. Association for Computing Machinery.

95

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

96

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

97

Robert Pollack.
The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions.
PhD thesis, Department of Computer Science, University of Edinburgh, April 1995.

98

D. Prawitz.
Natural Deduction.
Almquist and Wiksell, Stockholm, 1965.

99

Willard van Orman Quine.
Word and Object.
MIT Press, Cambridge, Massachusetts, 1960.

100

Thomas Reps.
Generating Language-Based Environments.
PhD thesis, Cornell University, Ithaca, New York, 1982.

101

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

102

J. C. Reynolds.
Towards a theory of type structure.
In B. Robinet, editor, Programming Symposium, Lecture Notes in Computer Science #19, pages 408-425, Berlin, 1974. Springer-Verlag.

103

Adrian Rezus.
Semantics of constructive type theory.
Technical Report 70, Informatics Dept., Nijmegen University, September 1985.

104

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

105

D. S. Scott.
Data types as lattices.
SIAM Journal on Computing, 5:522-87, 1976.

106

Anton Setzer.
Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe.
PhD thesis, Ludwig-Maximilians-Universität, München, September 1993.

107

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

108

S. Stenlund.
Combinators, $\lambda$-Terms, and Proof Theory.
D. Reidel, Dordrechte, 1972.

109

W. W. Tait.
Intensional interpretation of functionals of finite type.
Journal of Symbolic Logic, 32(2):189-212, 1967.

110

W. W. Tait.
Against intuitionism: Constructive mathematics is part of classical mathematics.
Journal of Philosophical Logic, 12:173-195, 1983.

111

Alfred Tarski.
The Concept of Truth in Formalized Languages, pages 152-278.
Clarendon Press, Oxford, 1956.
Translation of 1933 paper in Polish.

112

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

113

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

114

A. M. Ungar.
Normalization, Cut-elimination and the theory of proofs, Lecture Notes 28.
CLSI, Stanford, 1992.

115

Walter P. van Stigt.
Brouwer's Intuitionism.
North-Holland, Amsterdam, 1990.

116

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

117

Ludwig Wittgenstein.
Tractatus Logico-Philosophicus.
Routledge & Kegan Paul, London, 1922.

118

Ludwig Wittgenstein.
Philosophical Investigations.
Basil Blackwell, Oxford, 1953.

119

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

120

J. I. Zucker.
The correspondence between cut-elimination and normalization.
Annals of Mathematical Logic, 7:1-112, 1974.
Errata ibid 7, p.156.

121

J. I. Zucker.
Formalization of classical mathematics in Automath.
In Colloque International de Logique, pages 135-145, Paris, 1977. Colloques Internationaux du Centre National de la Recherche Scientifique, CNRS.