Extracting nondeterministic concurrent programs - Ulrich Berger (25th EACSL Annual Conference on Computer Science Logic (CSL 2016)., 2016)
We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of nondeterministic concurrent programsfrom proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.