The purpose of this paper is threefold. First, we describe some basic ideas of constructive type theory, with emphasis on their value for specification. Second, we demonstrate the use of type theory as a specification language. This is done by means of a detailed example, namely, the specification of an abstract data type (ADT) for multisets. (This example is a refinement of the multiset example in [3].) Finally, we describe how a theorem proving environment built on type theory can be used to aid in implementation of the ADT.