Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming (Q2640347)

The authors define attribute grammars and show that they can be used to give an operational semantics to recursive program schemes. They define a notion of partial correctness of an attribute grammar with respect to a specification and give an inductive method for proving partial correctness. They show how this can be applied to prove correctness of imperative, applicative or logic programs. The paper is clear and includes numerous examples.