- ...Automata
- Supported in part by NSF grants CCR-9423687, DUE-955162.
- ...mathematics.
- The library's url is www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html.
- ...mathematics
- Even worse, few people
appreciate that this is a significant new problem (see
[7]).
- ...Nuprl.
- Nuprl is free software that can be obtained from the Web site mentioned earlier. It runs on a freely available Allegro Common Lisp under Linux as well as free CMU Common Lisp under Unix.
- ....
- We
only need the universe of small types denoted simply
. For a full discussion of universes, see Allen
[1] as well as Jackson [20].
- ....
- A discussion of the constructive meaning of these types is beyond the scope of this work, but see [28][20][9].
- ....
- It might be better notation to overload
and write the relation as 
. We might change the library display to this at some point.
- ....
- Recall that
is the fully expanded notation for 
.