Chronological Index:

Imperative Program Semantics 
Stuart Allen, May 2, 1995 
SquareRoot Verification 
Jason Hickey, Mark Hayden, May 1995 
The Refiner as the Inference Mechanism of Nuprl Proof Development System 
Roderick Moten, April 4, 1995 
Defining the Polynomial Time Functions over N in Nuprl 
Robert L. Constable, March 28, 1995 
Developing Set Theory in HOL 
Paul Jackson, February 28, 1995 
Motivation: Basis of a Set Theory for Nuprl 
Todd Wilson, February 21, 1995 
Chet Says GoodBye: Theory; Implementation (System); Methodology; Science 
Chet Murthy, February 14, 1995 
Formal Methods Program at NASA Langley Research Center 
Jim Caldwell, February 7, 1995 
The Engineering Aspects of ProofEnvironment Design 
Chet Murthy, January 24, 1995 
Very Dependent Function Space 
Jason Hickey, Fall, 1994 
Notation and Computer Aided Mathematics 
Conal Mannion, December 6, 1994 
Verifying an Implementation of a Polynomial Algebra ADT 
Paul Jackson, November 29, 1994 
Representing Computational Complexity in Nuprl 
Robert L. Constable, November 22, 1994 
The "Interface" Version of Nuprl 
Stuart Allen and Rich Eaton, November 15, 1994 
The Ultimate Programming Machine, Part II 
Jason Hickey, November 8, 1994 
TLA 
Scott Stoller and Chet Murthy, November 1, 1994 
The Ultimate Programming Machine 
Jason Hickey, October 25, 1994 
Program Optimization in Type Theory 
Brent Knight, October 18, 1994 
Program Development for Proof Transformations 
Helmut Schwichtenberg, October 12, 1994 
Computer Algebra, Theorem Proving, and Types 
Todd Wilson, October 4, 1994 
Gröbner Basis 
Thomas Yan, September 20, 1994 
Recursive Types in Coq 
Christine PaulinMohring, Laboratoire de l'Informatique du Parallelisme, CNRS URA 1398, Ecole Normale Superieure de LyonFRANCE, September 8, 1994 