Extracting total Amb programs from proofs

TL;DR

This work introduces CFP, a Concurrent Fixed Point Logic that enables extraction of nondeterministic and concurrent programs with guaranteed totality and correctness. It builds on IFP by adding Restriction ($B|_{A}$) and a concurrent operator ($\mathbf{\downdownarrows}$), with Amb providing globally angelic nondeterminism; a two-stage denotational and an operational semantics are developed to ensure alignment between extracted programs and their specifications. Realizability-based interpretations (RIFP/RCFP) underpin the extraction process, providing soundness and data-soundness results that connect proofs to computable witnesses. The authors demonstrate practical utility by extracting a concurrent Gray-code to signed-digit converter, implemented in Haskell, and discuss broader implications for computable analysis and locally vs. globally angelic choice. Overall, CFP offers a rigorous framework for deriving provably correct concurrent programs from constructive proofs, with concrete applications and an implemented prototype.

Abstract

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: Restriction (binary), a strengthening of implication, and a unary 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.This is a revised and extended version of the conference paper presented at ESOP 2022 with the same title that contains full proofs of all major results.

Theorems & Definitions (64)

• Lemma 2.1
• proof
• Remark 2.2
• Example 1
• Lemma 2.3
• proof
• Lemma 3.1
• proof
• Lemma 3.2
• proof