  We present a logical system CFP (Concurrent Fixed Point Logic) from whose
proofs one can extract nondeterministic and concurrent programs that are
provably total and correct with respect to the proven formula. CFP is an
intuitionistic first-order logic with inductive and coinductive definitions
extended by two propositional operators, A || B (restriction, a strengthening
of the implication B -> A) and $\ddownarrow(A)$ (total concurrency). The target
of the extraction 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. The correctness of extracted programs is proven via an
intermediate domain-theoretic denotational semantics. We demonstrate the
usefulness of our system by extracting a concurrent program that translates
infinite Gray code into the signed digit representation. A noteworthy feature
of our system is 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.
