Research Initiation: Denotational Semantics in Absolute Logics of Programs

研究提出统一指称语义的编程语言与抽象模型理论的分支致力于绝对逻辑的研究。具体主题包括：Prolog和Lisp类程序设计语言指称语义的绝对形式的构造，Hoare式推理系统，程序验证方法的比较研究，绝对指称语义的论域理论，“n次”时态逻辑的验证能力。所提出的研究的主要影响之一是能够表征的绝对和相对的程序验证能力和价格（表示在所需的定理证明子程序的强度）的程序验证方法的Prolog和Lisp类编程语言，以及新的程序验证方法的建设。

Research is proposed unifying denotational semantics of programming languages with a branch of abstract model theory devoted to the study of absolute logics. Specific topics include: The construction of absolute versions of denotational semantics of Prolog- and Lisp- like programming languages Hoare-style inference systems, the comparative study of program verification methods, domain theory for absolute denotational semantics the verifying power of the "n times" temporal logics. One of the main impacts of the proposed research is the ability to characterize the absolute and relative program verifying power and price (expressed in the strength of the needed theorem prover subprogram) of program verification methods for Prolog- and Lisp- like programming languages as well as the construction of new program verification methods.