Research Initiation: Denotational Semantics in Absolute Logics of Programs

将程序设计语言的指称语义学与抽象模型论的一个分支统一起来，研究绝对逻辑。具体主题包括：类Prolog和Lisp编程语言的绝对指示语义的构建、hoore风格的推理系统、程序验证方法的比较研究、绝对指示语义的领域理论、“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.