Copenhagen Programming Language Seminar

An Observationally Complete Program Logic for Higher-Order Functions

Kohei Honda
Queen Mary, London, UK

Wedensday, October 3, 11:00-12:00
ITU , Rued Langgaards Vej 7, Room 4A.14

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 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.

Scientific host:Thomas Hildebrandt and Lars Birkedal The Programming, Logic and Semantics (PLS) research group at ITU.. Administrative host: Annette Enggaard . All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org