@INPROCEEDINGS{Basin91a,
AUTHOR        = {David Basin and Doug Howe},
TITLE         = {Some Normalization Properties of Martin-Lof's Type Theory, and Applications},
EDITOR        = {T. Ito and A.R. Meyer},
BOOKTITLE     = {International Conference on Theoretical Aspects of Computer Sof
tware (TACS '91)} 
PUBLISHER     = {Springer Verlag},
YEAR          = {1991},
SERIES        = LNCS,
VOLUME        = {526},
PAGES         = {475--494},
ABSTRACT      = {
For certain kinds of applications of type theories, the
faithfulness of formalization in the theory depends on intensional,
or structural, properties of objects constructed in the
theory. For type theories such as LF, such properties can
be established via an analysis of normal forms and types.
In type theories such as Nuprl or Martin-L\"of's polymorphic
type theory, which are much more expressive than LF, the
underlying programming language is essentially untyped,
and terms proved to be in types do not necessarily have
normal forms. Nevertheless, it is possible to show that
for Martin-L\"of's type theory, and a large class of extensions
of it, a sufficient kind of normalization property does
in fact hold in certain well-behaved subtheories. Applications
of our results include the use of the type theory as a logical
framework in the manner of LF, and an extension of the {\em
proofs-as-programs} paradigm to the synthesis of verified
computer hardware. For the latter application we point out
some advantages to be gained by working in a more expressive
type theory.  },
}