An extension of the simply-typed lambda calculus with constructs for expressing a notioncalled underdeterminism is studied. This allows us to interpret notions of stub and skeletonused in top-down program development. We axiomatise a simple notion of program refinement,and give a semantics, for which the calculus is proved sound and complete. An extension of the simply-typed lambda calculus with constructs for expressing a notioncalled underdeterminism is studied. This allows us to interpret notions of stub and skeletonused in top-down program development. We axiomatise a simple notion of program refinement, and give a semantics, for which the calculus is proved sound and complete.