This dissertation defines a Type Theory based semantics for Java-like reference type constructors. The primary focus is made on finding an adequate axiomatization of reference types in Type Theory. An extension of Type Theory, called {\em Reference Type Theory}, is introduced. It adds to the Type Theory language a reference type constructor and operations on reference type elements as primitive notions. The dissertation provides informal graph-based semantics for the Reference Type Theory, describes inference rules for this theory, and proves their consistency. Reference Type Theory is formalized in the Nuprl Proof Development System. This formalization is used to define a formal semantics for a fragment of the Java programming language and to verify several simple Java programs.