If you have a program and run it, then it usually shows some behaviour. This may take the form of interactions with a display, a printer, or communication ports. More closely looked, its main interactions may be with an operating system, libraries and other software. Anyway it has a certain behaviour, which can be useful, can be disastrous, or can be enjoyable.
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 an extension 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 and general 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.