In some programming languages, variables may refer to procedures; these references may be read to call the procedures and updated to refer to new procedures. If the procedures are recursive, it has been unknown whether there exists any “observationally complete” logic that can always prove if two programs have different behaviors.

The authors answer this question positively for programs in an imperative extension of call-by-value PCF (a typed, higher-order functional language). For this purpose, they extend a classical logic language by “evaluation formulas” that are able to specify the pre-/post-state relationships of programs. This is, in general, tricky because of the circularity of a recursive procedure P stored in a program variable x that may call the procedure stored in x under the assumption that x holds P itself. After presenting a sound proof calculus for their logic, the authors show that it is observationally complete by reducing every PCF program into a finite canonical form (FCF) from which a characteristic formula can be derived that captures the whole behavior of the FCF.

Apart from the formal details that represent the core of the paper, the authors give ample space to the general motivation of their work and provide various examples that make the material accessible. They also discuss in depth how their work is embedded in the existing corpus on complete logic for imperative languages with higher-order procedures. In particular, an early impossibility result implies that even under finite models (where first-order logic is decidable), their logic is undecidable.