Just in case this is of any interest to you, this is the abstract of the talk on logics I gave in Copenhagen. My thanks go to Lars Berkdale and Thomas Hildebrandt for hosting my talk.
Title:
An Observationally Complete Program Logic for Higher-Order Functions
Time and Place:
October 3rd, 11:15-12:30, ITU Copenhagen
Abstract:
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 extensions of Hoare logic to higher-order functions. Extending Hoare logic to higher-order functions (which also underlie such popular languages as Java) 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 strong 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 its extensions, and point out several remaining topics.
[end]
