Slides from
several talks
may be found at the bottom of this page.

Abstraction for Concurrent Objects

I Filipovic, PW O'Hearn, N Rinetzky and H Yang.
* Theoretical Computer Science, vol 411(51-52),* pp4379--4398, December 201
0.

Blaming the Client: On Data Refinement in the Presence of Pointers

I Filipovic, P O'Hearn, N Torp-Smith and H Yang.
* Formal Aspects of Computing 22(5)* pp 547-583, Sept 2010

Verifying Linearizability with Hindsight

PW O'Hearn, N Rinetzky, M Vechev, E Yahav, G Yorsh.
* PODC 2010*, pp85-94.

Graphical Models of Separation Logic

I Wehrman, T Hoare, P O'Hearn.
Information Processing Letters, June 2009.

Separation and Information Hiding.

P O'Hearn, H Yang and J Reynolds. * ACM TOPLAS 31(3), April 2009.* (Prelim
version appeared in POPL'04.)

Abstraction for Concurrent Objects

I Filipovic, PW O'Hearn, N Rinetzky and H Yang.
* ESOP'09 *

Compositional Shape Analysis by means of Bi-Abduction

C Calcagno, D Distefano, PW O'Hearn and H Yang.
* POPL'09 *.
Extended version to appear in J.ACM.

Separation Logic Semantics of Communicating Processes

T Hoare and P O'Hearn, Proceedings of 1st FICS conference, ENTCS, 2008.

Scalable Shape Analysis for Systems Code

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn.

In * CAV'08 *, pp385-398

Local Action and Abstract Separation Logic.

C Calcagno, PW O'Hearn and H Yang.
In * LICS'07 *.

Resources, Concurrency and Local Reasoning

PW O'Hearn,
* Theoretical Computer Science 375(1-3) *,
pp271-307, May 2007.

A
preliminary version appeared in the
Proceedings of CONCUR'04, LNCS 3170, pp49-67.

Festschrift for John C Reynolds's 70th Birthday.

* Theoretical Computer Science, Vol 375(1-3), * 1 May 2007.

Shape analysis for composite data structures.

J Berdine, C Calcagno, B Cook, D Distefano, PW O'Hearn, T Wies and H Yang.

In * CAV'07 *.

Footprint Analysis: A shape analysis that discovers preconditions.

C Calcagno, D Distefano, P O'Hearn and H Yang. In * SAS'07 *

Variance Analyses from Invariance Analyses (or, Termination Analyzers for Free!)

J Berdine, A Chawdhary, B Cook, D Distefano and P O'Hearn

POPL 2007

Modular Verification of a Non-blocking Stack

M Parkinson, R Bornat and P O'Hearn

POPL 2007

Strong Update, Disposal, and Encapsulation in Bunched Typing.

J Berdine and PW O'Hearn. MFPS 2006.

Verified Software: A Grand Challenge

C Jones, P O'Hearn and J Woodcock. IEEE Computer, March 2006, pp93-95.

Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic.

C Calcagno, D Distefano, P O'Hearn and H Yang. In * 13th SAS, LNCS 4134*,
182-203, 2006

Automatic termination proofs for programs with shape-shifting heaps.

J Berdine, B Cook, D Distefano and P O'Hearn.In * 18th CAV, LNCS 4144*, pp386-400, 2006

Smallfoot: Modular Automatic Assertion Checking with Separation Logic

J Berdine, C Calcagno and PW O'Hearn. In * 4th FMCO, LNCS 4111,* 2006

A
Collection of Example Smallfoot Programs

A local shape analysis based on separation logic

D Distefano, P O'Hearn and H Yang. In * 12th TACAS, LNCS 3920, pp287-302*, 2006.

Symbolic Execution with Separation Logic.

J Berdine, C Calcagno and PW O'Hearn. Proceedings of APLAS'05, LNCS 3780, pp52-68.

Permission Accounting in Separation Logic

R Bornat,
C Calcagno, P O'Hearn and M Parkinson

POPL 2005, 59-70.

A Decidable Fragment of Separation Logic

J Berdine, C Calcagno
and P O'Hearn

Proceedings of FSTTCS 2004, 97-109.

Refinement and Separation Contexts

I Mijajlovic, N Torp-Smith and
and P O'Hearn

FSTTCS 2004, 421-433.

Local Reasoning, Separation and Aliasing

R Bornat,
C Calcagno and P O'Hearn

In the informal proceedings of
SPACE 2004.

Separation and Information Hiding

PW O'Hearn,
H Yang and JC Reynolds

POPL'04, pages 268-280.

** Possible worlds and resources: The semantics of BI**

David Pym, Peter O'Hearn, Hongseok Yang

Theoretical Computer Science 315(1), pp257-305, 2004.

**
Program Logic and Equivalence in the Presence of Garbage Collection**

Cristiano Calcagno, Peter O'Hearn, Richard Bornat.
* Theoretical Computer Science, *
vol. 298/3, pp557-581, 2003.

** On Bunched Typing**

Journal of Functional Programming, 13(4), pp747-796, 2003.
PDF version

**Linear
Continuation-Passing **

Josh Berdine, Peter O'Hearn, Uday Reddy, Hayo Thielecke.

*Higher Order and Symbolic Computation,*
15(2/3):181--208, September 2002.

**
A Semantic Basis for Local Reasoning
**

Hongseok Yang, Peter O'Hearn

Proceedings of FOSSACS'02.
PDF version

**
Local Reasoning about Programs that Alter Data Structures
**

Peter O'Hearn, John Reynolds, Hongseok Yang

Proceedings of CSL'01, Paris, 2001. Pages 1-19, LNCS 2142
©Springer-Verlag.
PDF version

**
Computability and Complexity Results for a Spatial Assertion Language
for Data Structures
**

Cristiano Calcagno, Hongseok Yang, Peter O'Hearn

Proceedings of FSTTCS'01.
PDF version

** BI as an Assertion Language for Mutable Data Structures. **

Samin Ishtiaq, Peter O'Hearn

Proceedings of POPL'01.
PDF version

**Linearly Used Cont
inuations**

Josh Berdine, Peter O'Hearn, Uday Reddy, Hayo Thielecke

Proceedings of Continuations Workshop, 2001

Note: This paper has been superceded by ``Linear Continuation-Passing''.

**
On Garbage and Program
Logic**

Cristiano Calcagno, Peter O'Hearn

Proceedings of FOSSACS'01.

** Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare
Logic**

Cristiano Calcago, Samin Ishtiaq, Peter O'Hearn

Proceedings of PPDP'00.
PDF version

** From Algol to Polymorphic Linear Lambda-calculus**
(
postscript
)

P. W. O'Hearn and J. C. Reynolds

* Journal of the ACM *,
47(1), pp167-223, January 2000.

** Petri Net Semantics of Bunched Implications
**

Peter O'Hearn and Hongseok Yang
Unpublished Manuscript, 14 Oct, 1999

** The logic of bunched implications
**

P.W. O'Hearn and D. J. Pym. * Bulletin of Symbolic Logic *,
5(2), June 1999, pp215-244

** Resource Interpretations, Bunched Implications
and the alpha-lambda-calculus **

P. W. O'Hearn,
in J.-Y. Girard, ed.,
Proceedings, 4th Conference on Typed Lambda-Calculi and Applications, L'Aquila, Italy, April 1999. pages 258-279. LNCS 1581
©Springer-Verlag.

* Note: This paper has been superceded by ``On Bunched Typing''. *

** Bireflectivity. **

P. J. Freyd, P. W. O'Hearn, A. J. Power, R. Street, M. Takeyama and R. D. Tennent.

* Theoretical Computer Science * 228(1-2) 49-76, 1999.

Preliminary version appeared in
Proceedings of
MFPS XI.

** Syntactic Control of Interference Revisited ** .

P. W. O'Hearn, A. J. Power, M. Takeyama and R. D. Tennent.

* Theoretical Computer Science * 228(1-2) 211-252, 1999.

Preliminary version appeared in
Proceedings of
MFPS XI.

** Objects, Interference and the Yoneda Embedding** .

P. W. O'Hearn and U.S. Reddy.

* Theoretical Computer Science * 228(1-2) 253-282, 1999.

Preliminary version appeared in
Proceedings of
MFPS XI.

** Polymorphism, Objects and Abstract Types **

P. W. O'Hearn

* SIGACT News *, Volume 29(4), pp39-50, December 1998

** An Axiomatic Approach to Binary Logical Relations, with applications
to Data Refinement** .

Y. Kinoshita, P. O'Hearn, J. Power, M. Takeyama, R. Tennent,
TACS'97

©Springer-Verlag.

** Domains and Denotational Semantics: History, Accomplishments, and Open Problems ** .

M. P. Fiore, A. Jung, E. Moggi, P. O'Hearn, J. Riecke, G. Rosolini, and I. Stark.

In number 59 of * Bulletin of the European Association for
Theoretical Computer Science,* pages 227--256, 1996.

** Note on Algol and Conservatively Extending Functional Programming ** .
P. W. O'Hearn

J. Func. Programming, 6(1), pp171--180, January 1996.

** Kripke Logical Relations and PCF ** .

P. W. O'Hearn and J. G. Riecke.

Information and Computation,
120(1):107-116, 1995.

** Parametricity and Local Variables ** .

P. W. O'Hearn and R. D. Tennent.

* J.ACM. * 42(3): 658-709, May 1995.

**
Semantical analysis of specification logic, part 2
**.
* Abstract * .

P. W. O'Hearn and R. D. Tennent.

Information and Computation 107(1), pp25-57, 1993.

**
A model for Syntactic Control of Interference
**.

P. W. O'Hearn.

Mathematical Structures in Computewr Science, 1993.

** Semantics of Local Variables. **

P. W. O'Hearn and R. D. Tennent.

Applications of Categories in Computer Science, volume 177 of
the London Math Society Lecture Notes Steris, pp. 217-238, Cambridge Univ Press, 1992.

** Algol-like languages**

P.W. O'Hearn and R.D. Tennent editors

Progress in Theoretical Computer Science, Birkhauser, 1997

Tutorial on Separation Logic.

CAV Invited Tutorial, July 2008, Princeton

Space Invading Systems Code.

LOPSTR Invited Talk, July 2008, Valencia.
Short paper in the LOPSTR Proceedings

**
Resources, Concurrency and Local Reasoning
**

Slides from invited talk at ETAPS'04 .

**
Local Reasoning about Programs that Alter Data Structures. **

Peter O'Hearn, John Reynolds, Hongseok Yang

Slides from invited talk at CSL'01.

**
Reasoning about Shared Mutable Data Structure. **

John Reynolds, Peter O'Hearn

Slides from invited talk at
SPACE 2001.
PDF version

** Semantics of Storage**

Slides from Invited Lecture, MFPS00, Hoboken NJ.