一句话：提出从程序抽取视角出发、以经典正确性断言实现的构造性连续Domain理论，并给出函数空间与实数表示定理。
本文从程序抽取的视角建立连续Domain的构造性理论。其目标是使抽取出的程序表示可证明正确的计算，却不携带正确性见证；为此，作者以经典逻辑形式陈述正确性断言。技术上，论文从predomain基出发构造completion，并围绕Scott拓扑研究连续性，给出函数空间的构造。作者详细讨论主要动机例子，并将理论实例化到实数：将实数视为有理区间predomain之completion的全元素，进而证明一个表示定理，精确刻画可表示的连续函数类。
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.