Chronological Index:
1997-98
Spring Semester
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs
Brigitte Pientka, May 5, 1998
Intensional Polymorphism in Type-Erasure Semantics
Stephanie Weirich, April 28, 1998
Intuitionism - The Philosophy of L. E. J. Brouwer
Dirk Schlimm, Carnegie Mellon University, April 21, 1998
Simple, Efficient Object Encoding using Intersection Types
Karl Crary, April 14, 1998
Adding Intersection Types to Doug Howe's Classical Set-Theoretic Semantics
Evan Moran, April 7, 1998
Application of Notational Methods in dy/dx
Stuart Allen, March 31, 1998
Formal Models for Nuprl Evaluator
Alexey Nogin, March 24, 1998
Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System
Pavel Naumov, March 10, 1998
Logical Programming Environments
Jason Hickey, March 3, 1998
Type Methodology for Modern Languages and Compilers
Karl Crary, February 24, 1998
The Nuprl 5 Library
Rich Eaton, February 9, 1998
Dead Code Elimination
Ozan Hafizogullari and Christoph Kreitz, January 27, 1998
Fall Semester
A Uniform Rippling Approach for Instantiating Free Variables
Brigitte Pientka, December 2, 1997
References in Type Theory
Pavel Naumov, November 25, 1997
Extracting Readable and Efficient Programs from Nuprl Proofs
James Caldwell, November 18, 1997
Sociology of Proof
Professor Donald MacKenzie, Visitor from the University of Edinburgh, November 3, 1997
Abstract Identifiers in Nuprl 5 (continued)
Stuart Allen, October 28, 1997
Abstract Identifiers in Nuprl 5
Stuart Allen, October 21, 1997
Proof Polynomials: Cut Elimination
Sergei Artemov, October 7, 1997
SupInf
Tobias Mayr, September 23, 1997
From System F to Typed Assembly Language
Karl Crary, September 16, 1997
Reasoning about Java Classes in Nuprl (continued)
Pavel Naumov, September 16, 1997
Reasoning about Java Classes in Nuprl
Pavel Naumov, September 9, 1997