next up previous contents index
Next: Definitions Up: Components of the Previous: Components of the


The Nuprl system has six major components: a window  manager, a text  editor, a proof  editor, a library  module, a command  module and a function  evaluator. Interaction with Nuprl takes place in the context of three languages---the command  language, which is extremely simple, the object  language, which is the mathematical language of the system, and the metalanguage,  which is a programming language with data types referring to the object language. The command language is used to initiate editing, use the library and initiate executions in the object and metalanguages, to name a few of its functions. The object language is a constructive theory of types. The metalanguage is the programming language ML from the Edinburgh LCF system modified to suit Nuprl .

The window manager provides the interface for the interactive creation of certain kinds of linguistic objects called definitions, theorems, proofs and libraries on a terminal screen. Windows offer views of objects; using these views the user can navigate through the object, stopping to modify it, to copy parts of it to other windows or to insert parts into it from other windows, etc. Three special windows provide for editing theorems, viewing the library and entering commands.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995