Extracting Non-Deterministic Concurrent Programs
Ulrich Berger · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2016
We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of non-deterministic concurrent programs from proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.