9 papers:
LOPSTR-2001-Caldwell #recursion #type system- Extracting General Recursive Program Schemes in Nuprl’s Type Theory (JLC), pp. 233–244.
CADE-2000-AllenCEKL #logic- The Nuprl Open Logical Environment (SFA, RLC, RE, CK, LL), pp. 170–176.
CAV-1998-FeltyHS #protocol #verification- Protocol Verification in Nuprl (APF, DJH, FAS), pp. 428–439.
- CADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using
- Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
- CADE-1997-Hickey #framework #higher-order #implementation #logic #named
- Nuprl-Light: An Implementation Framework for Higher-Order Logics (JJH), pp. 395–399.
- CADE-1992-Chen #empirical #knowledge-based #proving #theorem proving
- Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.
- CAV-1992-AagaardL #case study #logic #synthesis #verification
- Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification (MA, ML), pp. 69–81.
- CADE-1988-Howe
- Computational Metatheory in Nuprl (DJH), pp. 238–257.
- CADE-1986-Howe #empirical #implementation
- Implementing Number Theory: An Experiment with Nuprl (DJH), pp. 404–415.
