Peter O'Hearn, Online Papers

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

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.

Resources, Concurrency and Local Reasoning
PW O'Hearn
Proceedings of CONCUR'04, LNCS 3170, pp49-67.

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

Talks

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.