The Book

Implementing Mathematics with The Nuprl Proof Development System

Preface

We hope to accomplish four things by writing this book. Our first goal is to offer a tutorial on the new mathematical ideas which underlie our research. In doing so we have tried to provide several entry points into the material, even at the cost of considerable redundancy. We hope that many of the ideas will be accessible to a well-trained undergraduate with a good background in mathematics and computer science. Second, parts of this book should serve as a manual for users of the Nuprl system (pronounced "new pearl"). As the system has grown so has the demand, both here at Cornell and at other institutions, for better documentation. We have tried to collect here all material relevant to the operation of the system. Third, we give an overview of our project for those interested in applications of the results and for those inclined to basic research in the area. Finally, we present new research which has arisen as we have worked on the Nuprl system. This system embodies contributions to the foundations of computer science and semantics, to automated reasoning and to system design, and it has shown promise as an intelligent system.

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 Nuprl.

Robert L. Constable
for the PRL Group
Ithaca, NY 1985

The Book

Implementing Mathematics with The Nuprl Proof Development System

Contents

Preface