@INPROCEEDINGS{Basin88a,
AUTHOR = "Basin, David",
TITLE = "Building Theories in Nuprl",
BOOKTITLE = "Logic At Botik, '89",
ADDRESS = "Pereslavl-Zalessky, USSR",
PUBLISHER = "Springer-Verlag",
YEAR = 1989,
PAGES = "12--25",
NOTE  = {Paper is extended version of conference paper},
ABSTRACT = {
This paper provides an account of how mathematical knowledge is
represented, reasoned about, and used computationally
in a mechanized constructive theorem proving
environment.  We accomplish this by presenting a
particular theory developed in the Nuprl proof
development system: finite set theory culminating in
Ramsey's theorem.  We believe that this development is
interesting as a case study in the relationship
between constructive mathematics and computer science.
Moreover, the aspects we emphasize --- the high-level
development of definitions and lemmas, the use of
tactics to automate reasoning, and the use of type
theory as a programming logic --- are not restricted
in relevance to this particular theory, and indicate
the promise of our approach for other branches of
constructive mathematics.  },
 }