The significance of type theory to the theory of programming languages has long
been recognized.  Advances in programming languages have often derived from
understanding that stems from type theory.  However, these applications of type
theory to practical programming languages have been indirect; the differences
between practical languages and type theory have prevented direct connections
between the two.

This dissertation presents systematic techniques directly relating practical
programming languages to type theory.  These techniques allow programming
languages to be interpreted in the rich mathematical domain of type theory.
Such interpretations lead to semantics that are at once denotational and
operational, combining the advantages of each, and they also lay the foundation
for formal verification of computer programs in type theory.

Previous type theories either have not provided adequate expressiveness to
interpret practical languages, or have provided such expressiveness at the
expense of essential features of the type theory.  In particular, no previous
type theory has supported a notion of partial functions (needed to interpret
recursion in practical languages), and a notion of total functions and objects
(needed to reason about data values), and an intrinsic notion of equality
(needed for most interesting results).  This dissertation presents the first
type theory incorporating all three, and discusses issues arising in the design
of that type theory.

This type theory is used as the target of a type-theoretic semantics for a
expressive programming calculus.  This calculus may serve as an internal
language for a variety of functional programming languages.  The semantics is
stated as a syntax-directed embedding of the programming calculus into type
theory.

A critical point arising in both the type theory and the type-theoretic
semantics is the issue of admissibility.  Admissibility governs what types it is
legal to form recursive functions over.  To build a useful type theory for
partial functions it is necessary to have a wide class of admissible types.  In
particular, it is necessary for all the types arising in the type-theoretic
semantics to be admissible.  In this dissertation I present a class of
admissible types that is considerably wider than any previously known class.