We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions.

翻译：我们从程序提取的角度来发展一个连续域的建设性理论。我们的目标是,在没有正确性证人的情况下,程序代表(可能正确)计算,我们的目标是通过形成典型的正确性声明来实现的。技术上,我们从前空基开始,构建一个完成点。然后我们调查斯科特地形的连续性,然后提出功能空间的构造。然后我们详细讨论我们的主要激励范例,然后将我们的理论转换为真实数字,我们把实际数字概念化为完成合理间隔前空点的全部要素,并证明代表的理论准确界定了可代表的连续功能的类别。