PRL Seminars 1998-99

Abstract

Stuart Allen presented a case study in which Nuprl was used to prepare a set of informal notes on a semantics for the language of Gries and Schneider's book on discrete math. (The semantics was developed in collaboration with Rick Aaron.)

Informal documents were prepared in Nuprl, but incorporating formal notation where precision is desired. Nuprl display system and definition system are exploited. Most of the operators are declared primitive and most of the proofs are Fiated in their substantial parts; the bulk of these short proofs simply being used for type checking. Some operators are defined, however, and some proofs were developed slighty further, when economical.

Some editing utilities were employed to assist in translating between object and meta expressions, in order to reduce errors.