A program logic allows us to describe such software behaviour using logical assertions. It often also enables syntactic derivation of valid descriptions. Such a logic may as well have a semantic basis, in the sense that its assertions discuss all and only observable behaviour of programs. One of the well-known logics with this property is Hoare's logic for first-order imperative programs, developed on the basis of Floyd's assertion method.

This talk is about extensions of Hoare logic to higher-order functions. Extending Hoare logic to higher-order functions has been known to be one of the subtle issues for decades:
this work uses ideas from the pi-calculus to develop such an extension. The logic allows clean, precise description of higher-order behaviour and has several completenesss properties. In this talk, I will illustrate core ideas of the logic using simple examples, discuss its completeness properties and their proof methods, position them among related works, and point out several remaining topics.