Copenhagen Programming Language Seminar
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:
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org