Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Peter O'Hearn
Peter O'Hearn
Professor of Computer Science, Queen Mary, University of London
News
Separation Logic for Concurrency
.
Quite a lot of recent interest surrounds concurrency.
Some highlights: we can transfer portions of heap between processes,
as in a resource manager or in efficient message passing;
we can do modular reasoning in the presence of semaphores (e.g.,
split binary semaphores without maintaining a global invariant);
we do parallel mergesort with no rely or guarantee conditions, the proven
processes
automatically mind their own business.
Permission Accounting in Separation Logic, by R Bornat,
C Calcagno, P O'Hearn and M Parkinson. To appear in POPL'05.
Includes a discussion
of ``resourcing'', the next big wave beyond typing according to Richard Bornat.
Steve Brookes and I gave a joint tutorial at
CONCUR'04 .
My research interests are in logic and semantics of computation, both the foundations
and applications thereof. Most recently this has concentrated on
local reasoning , where
a specification and proof
can concentrate on a circumscribed collection of
resources that a program actually acts upon, instead of the
entire conceivable state space of a system.
The key tools underlying this project are the logic of bunched implications,
developed with David Pym, and separation logic, developed with John Reynolds,
Hongseok Yang, and others.