Recursive programs and denotational semantics in absolute logics of programs (Q2639051)

A nonstandard or absolute (in the sense of Kripke-Platek) version of denotational semantics for recursive programs is given along with the corresponding absolute version of first-order dynamic logic, for which completeness is proven. Essentially this logic contains no unbounded quantifiers by the use of extra sorts, so that every formula has an explicit denotation in the model. The main interest of this logic is to provide a basis for a comparison of program verification methods for recursive programs.