  We present a logical system CFP (Concurrent Fixed Point Logic) supporting the
extraction of nondeterministic and concurrent programs that are provably total
and correct. CFP is an intuitionistic first-order logic with inductive and
coinductive definitions extended by two propositional operators: Rrestriction,
a strengthening of implication, and an operator for total concurrency. The
source of the extraction are formal CFP proofs, the target is a lambda calculus
with constructors and recursion extended by a constructor Amb (for McCarthy's
amb) which is interpreted operationally as globally angelic choice and is used
to implement nondeterminism and concurrency. The correctness of extracted
programs is proven via an intermediate domain-theoretic denotational semantics.
We demonstrate the usefulness of our system by extracting a nondeterministic
program that translates infinite Gray code into the signed digit
representation. A noteworthy feature of CFP is the fact that the proof rules
for restriction and concurrency involve variants of the classical law of
excluded middle that would not be interpretable computationally without Amb.
