The use of safety-critical software relies crucially on the certified verification relative to an unambiguous specification that the software will perform correctly, even on the first occasion it is put to use. One way of achieving unambiguity and assurance is to use mathematical or formal methods in the development process of such software, so that the result is software that is mathematically proven correct relative to a formal specification. The concept of algebraic specification refinement embodies a framework in which to develop software formally. In this thesis, this concept is expressed in a different, and in many respects, richer mathematical framework, namely that of type theory, polymorphic lambda-calculus, and an intuitionistic logic extended to assert relational parametricity, as well as key features of specification refinement. This translation into a different framework enables important extensions to the concept of algebraic specification refinement that enhance the proving power, the applicability, and hence the usefulness of the concept.