We give a canonical program refinement calculus based on the lambda calculus
and classical first-order predicate logic, and study its proof theory and
semantics. The intention is to construct a metalanguage for refinement
in which basic principles of program development can be studied. The calculus
is proven sound and complete with respect to a set-theoretic semantics.
The idea is that it should be possible to induce a refinement calculus
in a generic manner from a programming language and a program logic. For
concreteness, we adopt the simply-typed lambda calculus augmented with
primitive recursion as a paradigmatic typed functional programming language,
and use classical first-order logic as a simple program logic. A key feature
is the construction of the refinement calculus in a modular fashion, as
the combination of two orthogonal extensions to the underlying programming
language (in this case, the simply-typed lambda calculus). The crucial
observation is that a refinement calculus is given by extending a programming
language to allow indeterminate expressions (or `stubs') involving the
construction `some program *x *such that *P*'. Factoring this
into `some *x...*' and `... such that *P*', we first study extensions
to the lambda calculus providing separate analyses of what we might call
`true' stubs, and structured specifications. The questions we are concerned
with in these calculi are how do stubs interact with the programming language,
and what is a suitable notion of structured specification for program development.
The full refinement calculus is then constructed in a natural way as the
combination of these two subcalculi. The claim that the subcalculi are
orthogonal extensions to the lambda calculus is justified by a result that
a refinement can actually be factored into simpler judgements in the subcalculi,
that is, into logical reasoning and simple decomposition. The semantics
for the calculi are given using Henkin models with additional structure.
Both simply-typed lambda calculus and first-order logic are interpreted
using Henkin models themselves. The two subcalculi require some extra structure
and the full refinement calculus is modelled by Henkin models with a combination
of these extra requirements. There are soundness and completeness results
for each calculus, and by virtue of there being certain embeddings of models
we can infer that the refinement calculus is a conservative extension of
both of the subcalculi which, in turn, are conservative extensions of the
lambda calculus.