Concurrency Theory Workshop:
Reasoning about Separation, Resource,
Interference, Atomicity, OWHY.
Dates: 13-14 Jan 2009
Location: Robin Brook Centre, West Smithfield Campus, Queen Mary, Univ of London
Nearest underground stations are Farringdon and St Paul's.
Map 1
Map 2
Organizers: Peter O'Hearn, Matthew Parkinson
Note: An excellent successor workshop was hosted by Joey Coleman and Cliff Jones in Newcastle, the
Northern Concurrency Workshop
in Nov 2009.
This meeting is born of the close geographical, and even sometimes conceptual
and technical, proximity of people who have recently made
fresh advances on the theory of
concurrency.
Anyone is welcome to attend, but the
the talks will be aimed at experts, and there will be no expository presentations.
Background
It would help to
know (of) things like separation logic, rely-guarantee, process algebras,
and modal logics and type systems for processes.
Talks are scheduled for 30min,
with ample time set aside separately for discussion.
Note that the talks are in different rooms on the different days.
Schedule
Tuesday 13 Jan, Bainbridge Room, Robin Brook Centre
-
10:45am. Welcome (Coffee, tea, etc)
-
11:00am. Cliff Jones (Newcastle). A rational development of an ACM implementation (Simpson's 4-slot).
Slides
-
11:30am. Viktor Vafeiadis (MSR Cambridge). Some techniques for proving linearizability.
Slides
-
12:00noon. Discussion
-
12:30pm. Lunch
-
2:00pm. David Pym (HP Labs, Bristol). A Logical and Computational Theory of Located Resource. Slides
-
2:30pm. Matthew Hennessy (Trinity College Dublin). A resource aware pi calculus.
Slides
-
3:00pm. Discussion.
-
3:30pm. Break .
-
4:00pm. Thomas Dinsdale-Young (Imperial). Reasoning about concurrent B-trees.
Slides
-
4:30pm. Hongseok Yang (Queen Mary). Abstraction for concurrent objects.
Slides
-
5:00pm. Discussion
Wednesday 14 Jan, Paul Garrod Lecture Theatre, Robin Brook Centre
-
9:45am. Welcome (coffee, tea, etc)
-
10:00am. Nobuko Yoshida (Imperial). Global progress in multiparty session
types. Slides
-
10:30am. Julian Rathke (Southampton). Permission-based separation logic
for message passing concurrency.
Slides
-
11:00am. Discussion
-
11:30am. Peter Sewell (Cambridge). Relaxed Memory
Slides
-
12:00noon. Lunch.
-
2:00pm. Joey Coleman (Newcastle).
Fine-grained concurrent expression evaluation and rely/guarantee reasoning.
Slides
-
2:30pm. Mike Dodds (Cambridge). Deny-guarantee reasoning.
Slides
-
3:00pm. Tony Hoare (Microsoft). Graphical models of separation logic.
Slides
Other materials related to Hoare's presentations:
3:30pm. Coffee
4:00pm-5:15pm. Discussion.