(some pages have been annotated with links to more modern material pertaining to Nuprl4)
Authoring this book was a collective task; many individual efforts found their ways into these pages. Most chapters have several authors. That we were able to proceed in this fashion owes to the fact that we have assembled at Cornell a unique group of computer scientists who had worked for more than two years on the project.
We would like to acknowledge warmly the special contributions of Joseph L. Bates to this enterprise. Joe has been a chief architect of this system and was a major force in creating the PRL project, from which the system emerged. This manuscript is replete with Joe's ideas. We also want to thank Evan Steeg, who joined the project as an undergraduate and has since contributed significantly to our efforts, especially in the area of writing tactics. Tim Griffin's implementation of the rules for recursive types and partial functions is greatly appreciated as is his contribution of a new interface to the evaluator. All of our efforts are built on the contributions of Fran Corrado, our only full--time programmer. We also thank Christoph Kreitz, who has used the system extensively and provided us with insightful reports on its strengths and weaknesses. We also appreciate the constructive criticism of James Hook, who spent many hours reading and discussing early drafts. We thank Ryan Stansifer, Hal Perkins, and Aleta Ricciardi for proof--reading. Finally, we thank Donette Isenbarger, Michele Fish and Dawn Hall for their conscientious assistance in preparing the manuscript.
We appreciate the help we have received from the National Science Foundation through a series of grants supporting the Nuprl project, the Cornell Computer Science Department computing facility, and various pieces of equipment needed for this research (MCS80-03349, MCS81-04018, DCR80-03327, DCR81-05763, and DRC84-06052). The NSF has also supported Mr. Cleaveland and Mr. Smith with fellowships. We also appreciate the generous support of IBM, whose fellowships have supported Mr. Mendler. Finally, we acknowledge the support of Cornell University and especially our department for providing fellowships, matching funds, and the environment to make this work possible.
This is the first version of the manual. We consider it to be a preliminary effort and welcome timely comments that will help us improve the presentation. The manual describes version 1.0 of .
Robert L. Constable
for the PRL Group
Ithaca, NY 1985