85
Voted
ENTCS
2000
15 years 4 hour ago
2000
The NuPRL system [3] was designed for interactive writing of machine
96
Voted
JAPLL
2006
15 years 4 days 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...
93
Voted
TPHOL
1996
IEEE
15 years 4 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 ...
91
Voted
KBSE
1997
IEEE
15 years 4 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...
95
Voted
CADE
2000
Springer
15 years 4 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...