Copenhagen Programming Language Seminar


Separation Logic for Higher-order Typed Languages

Neel Krishnaswami,
Carnegie Mellon University

Thursday, March 23rd, 15:15-16:00 (!)
IT University of Copenhagen, Rued Langgaards Vej 7, auditorium 4


Separation logic is an extension of Hoare logic which permits reasoning about low-level imperative programs that use shared mutable heap structure. In this work, we create an extension of separation logic that permits effective, modular reasoning about typed, higher-order functional programs that use aliased mutable heap data, including pointers to code.

Scientific host: Lars Birkedal. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by 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