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