Theory
Mechanizing the Proof of Correction of a Compiler Using Type Theory
Yves Bertot, Visitor from INRIA, November 17, 1998
References in Type Theory
Pavel Naumov, November 25, 1997
CZF, Type Theory, and Nuprl-Light.
Robert L. Constable, April 1997
CZF, Type Theory, and Nuprl-Light
Evan Moran, April 8, 1997
Advancing the Type-Theoretic Underpinnings of Practical Programming Languages
Karl Crary, February 1997
Formal Objects in Type Theory.
Jason Hickey, September 1996
Formal Domain Theory
Neal Glew, December 5, 1995
Developing Set Theory in HOL
Paul Jackson, February 28, 1995
Program Optimization in Type Theory
Brent Knight, October 18, 1994
Formalizing the Theory Concept in Nuprl
Jason Hickey, March 1994
Formalizing the Theory Mechanism in NuPRL
Jason Hickey, March 15, 1994
A Basis for Constructive, Reflexive Type Theory
Bill Aitken, October 1, 1990
Department of Computer Science, Cornell University, Ithaca, NY.