The Milner-Damas type system, on which most functional programming languages rely, prohibits programs that go wrong, but allows programs that busy-loop or dead-lock, i.e., it allows programs that compute bottom.

 This thesis explores a strengthening of Milner-Damas that also prohibits bottom-computing programs: it develops a type system that guarantees termination for computations of finite values, such as lists, and productivity for computations of infinite values, such as streams.

 The core of the type system is a typing rule for fix with a built in proof principle that applies to both these classes of proofs. The principle is {\it induction on the size of a type}, where the size of a type is a bound on the heights of its values , or, for function types, a bound on the domains and co-domains of its values. The choice of proof is by the type assigned to a program: types that only contain finite values give termination proofs; types that only contain infinite values give productivity proofs. To express such types, a non-standard model, in which types denote upwards- rather that downwards-closed sets of program values, is introduced. All derivation rules of the type system are justified by this model.

 The thesis defines a pure, higher-order, lazy, functional programming language in which this type system is integrated; it defines a type checking algorithm for this langauge, and explores the language's pragmatics. Because type systems allow compositional proofs, termination and productivity can be guaranteed for arbitrarily large programs. Despite its stronger type system, the language is expressive enough to be used for embedded-systems programming: an application domain in which busy-loops and dead-locks are particularly disastrous.