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.

翻译：我们提出了一个逻辑系统CFP（并发不动点逻辑），支持提取可证明为全函数且正确的非确定性与并发程序。CFP是一个直觉主义一阶逻辑，包含归纳与余归纳定义，并扩展了两个命题算子：限制算子（一种强化的蕴含）和全并发算子。提取的源是CFP形式证明，目标是一个带有构造子和递归的λ演算，其扩展了一个构造子Amb（对应于McCarthy的amb），该构造子在操作语义上被解释为全局天使选择，并用于实现非确定性与并发。提取程序的正确性通过中间域论指称语义得到证明。我们通过提取一个将无限格雷码转换为带符号数字表示的非确定性程序，展示了该系统的实用性。CFP的一个显著特征是：限制与并发规则的证明涉及经典排中律的变体，若无Amb，这些规则在计算上是不可解释的。