Chronological Index:

Spring Semester

Imperative Program Semantics
Stuart Allen, May 2, 1995
Square-Root 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 Good-Bye: 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 Proof-Environment Design
Chet Murthy, January 24, 1995

Fall Semester

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
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 Paulin-Mohring, Laboratoire de l'Informatique du Parallelisme, CNRS URA 1398, Ecole Normale Superieure de Lyon-FRANCE, September 8, 1994