Program development in the constructive set theory TK
Martin C. Henson · Formal Aspects of Computing · 1989
Abstract 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.