摘要
An extension of the simply-typed lambda calculus with constructs for expressing a notion calledunderdeterminism is studied. This allows us to interpret notions of stub and skeleton used 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 notion calledunderdeterminism is studied. This allows us to interpret notions of stub and skeleton used 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.
