Using Nuprl as a Formal Assistant for Preparing Largely Informal Material

by Stuart F. Allen
1998-1999

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.

Using Nuprl as a Formal Assistant for Preparing Largely Informal Material

by Stuart F. Allen 1998-1999

by Stuart F. Allen
1998-1999