[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

NU Programming Languages Seminar
Wednesday, December 3, 2003
206 Egan  Hall, Northeastern University
    (building 60 on http://www.campusmap.neu.edu/)  
1145-145. Bring your lunch.

Dale Vaillancourt

Northeastern University

will present

Separation Logic:  A Logic for Shared Mutable Data Structures, by John
Reynolds

Abstract:

In joint work with Peter O'Hearn and others, based on early ideas of
Burstall, we have developed an extension of Hoare logic that permits
reasoning about low-level imerative programs that use shared mutable data
structures.
The simple imperative programming language is extended with commands for
accessing and modifying shared structures, and for explicit allocation and
deallocation of storage.  Assertions are extended by introducing a
``separating conjunction'' that asserts that its subformulas hold for
disjoint parts of the heap, and a closely related ``separating
implication''.  Coupled with the inductive definition of predicates on
abstract data structures, this extension permits thte concise and flexible
description of structures with controlled sharing."


-Mitch

Upcoming Events:

12/10??: Phillipe Meunier (This talk may be deferred to sometime in January).

1/7/04: Harry Mairson

Later in January:

Greg Pettyjohn: Comparing Web Servlet Technologies

--Mitch