/nyu p*rl/ Nearly Ultimate PRL.

A system for interactive creation of formal mathematics, including definitions and proofs. It has an extremely rich type system, including dependent functions, products, sets, quotients and universes. Types are first-class citizens. It is built on Franz Lisp and Edinburgh ML.

["Implementing Mathematics in the Nuprl Proof Development System", R.L. Constable et al, P-H 1986].

Last updated: 1994-12-13

Try this search on Wikipedia, OneLook, Google

Nearby terms: number sign « numeric keypad « Numeris « Nuprl » NU-Prolog » nurbs » Nu Thena


Copyright Denis Howe 1985 General Business Directory.