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.