Extracting total Amb programs from proofs

TL;DR

This paper introduces CFP, a logical system enabling extraction of total, correct concurrent programs from proofs, using a novel Amb operator for angelic choice, demonstrated through a Gray code translation example.

Contribution

The paper presents CFP, a new logic with operators for concurrency and totality, and a method to extract correct concurrent programs with angelic choice from proofs.

Findings

Extraction of a concurrent Gray code translation program

CFP's proof rules incorporate classical logic principles without losing computational interpretability

Operational semantics for Amb ensures correctness of extracted programs

Abstract

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.