Extracting total Amb programs from proofs

TL;DR

This paper introduces CFP, a logical system that enables the extraction of provably total, correct, nondeterministic, and concurrent programs from formal proofs, incorporating a novel Amb operator for concurrency.

Contribution

The paper presents CFP, a new logic with operators for restriction and total concurrency, and demonstrates program extraction with a focus on nondeterminism and concurrency.

Findings

Extracted a nondeterministic program translating Gray code to signed digit representation.

CFP supports program extraction from proofs involving classical logic variants.

The correctness of extracted programs is established via domain-theoretic semantics.

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 is 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.