Conference paper
Recursion in logics of programs
Abstract
The problem of reasoning about recursive programs is considered. Utilizing a simple analogy between iterative and recursive programs viewed as unfimte unions of finite terms, we carry out an investigation analogous to that carried out recently for iterative programs. The main results are the arithmetical completeness of axiom systems for (1) context-free dynamic logic and (2) its extension for dealing with infinite computations. Having the power of expression of these logics in mind, these results can be seen to supply (as corollaries) complete proof methods for the various kinds of correctness of recursive programs.
Related
Conference paper
Computable queries for relational data bases
Conference paper
Structure and complexity of relational queries
Paper