Description:
<jats:title>Abstract</jats:title>
<jats:p>We present a constructive theory of types and kinds designed with program development as the major desideratum. We show how this theory may be employed to derive programs from proofs of specifications (that is, demonstrations that specifications are satisfiable) and how the infrastructure of the theory supports the transformational development of programs in a natural way.</jats:p>