The burgeoning interest in concurrent computation has sparked an increased interest in theoretical models of concurrency. While standard sequential programming has a well-understood semantics and proof theory, the nondeterministic nature of concurrency has made a similar understanding of concurrent programming extremely difficult. Much interesting work in the field has been done, and much remains yet to be done; it is our intention in this paper to present a different kind of model of concurrency, a type-theoretic one, which we hope will shed light on reasoning about concurrency. We encode the synchronization tree model of Milner's CCS as a type in the Nuprl Type Theory. This is a constructive type theory equipped with a rich collection of inference rules for reasoning about types. We relate the equality in the type of synchronization trees with various behavioral equivalences. We also discuss the relation between the logic induced by our models and various modal logics for reasoning about concurrency.