Chronological Index:
1998-99
Spring Semester
A Methodology for Designing Asynchronous Circuits
Rajit Manohar, May 10, 1999
Some Uses of the Intersection Type
Stuart Allen and Robert L. Constable, May 3, 1999
The Current Projects of the MetaPRL Group
Alexey Nogin and Jason Hickey, April 26, 1999
Knowledge-Based Proof Planning
Erica Melis, April 19, 1999
Practical Uses of Quotations, Macros and Reflection
Eli Barzilay, April 5, 1999
Using Nuprl as a Formal Assistant for Preparing Largely Informal Material
Stuart Allen, March 29, 1999
Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics
and
Type Theory in a Membership Equational Logic Framework
Mark-Oliver Stehr, March 15, 1999
Importing Isabelle Formal Mathematics into NuPRL
Pavel Naumov, March 8, 1999
Typed Assembly Language
Neal Glew, March 1, 1999
A Formal Framework for Modeling Memory
Victor Luchangco, Visitor from MIT, February 22, 1999
A Programming Environment for Building Reliable High Performance Systems
Jason Hickey, February 15, 1999
Speeding Up the MetaPRL Refiner
Alexey Nogin, February 8, 1999
Verbalization of High-Level Formal Proofs
Amanda Holland-Minkley, February 1, 1999
Fall Semester
Semantics and Pragmatics of Reflected Proof
Stuart Allen, Sergei Artemov, and Robert L. Constable, December 1, 1998
On the Reflection Mechanism in Nuprl
Sergei Artemov, November 24, 1998
Mechanizing the Proof of Correction of a Compiler Using Type Theory
Yves Bertot, Visitor from INRIA, November 17, 1998
Reflection Mechanisms in Nuprl
Stuart Allen, Robert L. Constable, November 10, 1998
Automatic Debugging Through Type Inference, Continued
Ozan Hafizogullari, November 3, 1998
On Modeling Ensemble
Robert Constable, Jason Hickey, October 27, 1998
Listening to Theorem Provers who Talk to Each Other about Computer Systems
Robert L. Constable, October 20, 1998
Automatic Debugging Through Type Inference
Ozan Hafizogullari, October 6, 1998
On Howe's Importation of HOL into Nuprl
Evan Moran, September 29, 1998
On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis
Uwe Egly, Visitor from Technische Universitaet Wien, September 22, 1998
Automated Complexity Analysis
Ralph Benzinger, September 15, 1998
iPRL: A General Approach to Interpreting Isabelle Results in NuPRL
Pavel Naumov, September 8, 1998