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.
