ENTCS
2000
13 years 4 months ago
2000
The NuPRL system [3] was designed for interactive writing of machine
JAPLL
2006
13 years 4 months ago
2006
For twenty years the Nuprl ("new pearl") system has been used to develop software systems and formal theories of computational mathematics. It has also been used to expl...
TPHOL
1996
IEEE
13 years 8 months ago
1996
IEEE
Nuprl and HOL are both tactic-based interactive theorem provers for higher-order logic, and both have been used in many substantial applications over the last decade. However, the ...
KBSE
1997
IEEE
13 years 8 months ago
1997
IEEE
Proofs in the Nuprl system, an implementation of a constructive type theory, yield “correct-by-construction” programs. In this paper a new methodology is presented for extract...
CADE
2000
Springer
13 years 8 months ago
2000
Springer
Abstract. The Nuprl system is a framework for reasoning about mathematics and programming. Over the years its design has been substantially improved to meet the demands of large-sc...