Peter W. O'Hearn

Andrew P. Black, Peter W. O'Hearn: Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview. POPL 2012: 1-2

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: Verification Condition Generation and Variable Conditions in Smallfoot. CoRR abs/1204.4804 (2012)

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Compositional Shape Analysis by Means of Bi-Abduction. J. ACM 58(6): 26 (2011)

Peter W. O'Hearn: Algebra, Logic, Locality, Concurrency. APLAS 2011: 17-18

C. A. R. Hoare, Akbar Hussain, Bernhard Möller, Peter W. O'Hearn, Rasmus Lerchedahl Petersen, Georg Struth: On Locality and the Exchange Law for Concurrent Processes. CONCUR 2011: 250-264

Peter W. O'Hearn: Algebra, Logic, Locality, Concurrency. CPP 2011: 3-4

Peter W. O'Hearn: Reasoning about Programs Using a Scientific Method. ICFEM 2011: 14

Nikos Gorogiannis, Max I. Kanovich, Peter W. O'Hearn: The Complexity of Abduction for Separated Heap Abstractions. SAS 2011: 25-42

Ivana Filipovic, Peter W. O'Hearn, Noah Torp-Smith, Hongseok Yang: Blaming the client: on data refinement in the presence of pointers. Formal Asp. Comput. 22(5): 547-583 (2010)

Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51-52): 4379-4398 (2010)

Peter W. O'Hearn: Abductive, Inductive and Deductive Reasoning about Resources. CSL 2010: 49-50

Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, Greta Yorsh: Verifying linearizability with hindsight. PODC 2010: 85-94

Gary T. Leavens, Peter W. O'Hearn, Sriram K. Rajamani (Eds.): Verified Software: Theories, Tools, Experiments, Third International Conference, VSTTE 2010, Edinburgh, UK, August 16-19, 2010. Proceedings. Lecture Notes in Computer Science 6217, Springer 2010, isbn 978-3-642-15056-2

Ian Wehrman, C. A. R. Hoare, Peter W. O'Hearn: Graphical models of separation logic. Inf. Process. Lett. 109(17): 1001-1004 (2009)

Peter W. O'Hearn, Hongseok Yang, John C. Reynolds: Separation and information hiding. ACM Trans. Program. Lang. Syst. 31(3) (2009)

Ivana Filipovic, Peter W. O'Hearn, Noam Rinetzky, Hongseok Yang: Abstraction for Concurrent Objects. ESOP 2009: 252-266

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Compositional shape analysis by means of bi-abduction. POPL 2009: 289-300

Tony Hoare, Peter W. O'Hearn: Separation Logic Semantics for Communicating Processes. Electr. Notes Theor. Comput. Sci. 212: 3-25 (2008)

Peter W. O'Hearn: Tutorial on Separation Logic (Invited Tutorial). CAV 2008: 19-21

Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn: Scalable Shape Analysis for Systems Code. CAV 2008: 385-398

Peter W. O'Hearn: Separation Logic Tutorial. ICLP 2008: 15-21

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Space Invading Systems Code. LOPSTR 2008: 1-3

Olivier Danvy, Peter W. O'Hearn, Philip Wadler: Preface. Theor. Comput. Sci. 375(1-3): 1-2 (2007)

Peter W. O'Hearn: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3): 271-307 (2007)

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang: Shape Analysis for Composite Data Structures. CAV 2007: 178-192

Peter W. O'Hearn: Separation logic and concurrent resource management. ISMM 2007: 1

Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang: Local Action and Abstract Separation Logic. LICS 2007: 366-378

Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, Peter W. O'Hearn: Variance analyses from invariance analyses. POPL 2007: 211-224

Matthew J. Parkinson, Richard Bornat, Peter W. O'Hearn: Modular verification of a non-blocking stack. POPL 2007: 297-302

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Footprint Analysis: A Shape Analysis That Discovers Preconditions. SAS 2007: 402-418

Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock: Verified Software: A Grand Challenge. IEEE Computer 39(4): 93-95 (2006)

Josh Berdine, Peter W. O'Hearn: Strong Update, Disposal, and Encapsulation in Bunched Typing. Electr. Notes Theor. Comput. Sci. 158: 81-98 (2006)

Josh Berdine, Byron Cook, Dino Distefano, Peter W. O'Hearn: Automatic Termination Proofs for Programs with Shape-Shifting Heaps. CAV 2006: 386-400

Peter W. O'Hearn: Separation Logic and Program Analysis. SAS 2006: 181

Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, Hongseok Yang: Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. SAS 2006: 182-203

Dino Distefano, Peter W. O'Hearn, Hongseok Yang: A Local Shape Analysis Based on Separation Logic. TACAS 2006: 287-302

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: Symbolic Execution with Separation Logic. APLAS 2005: 52-68

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. FMCO 2005: 115-137

Richard Bornat, Cristiano Calcagno, Peter W. O'Hearn, Matthew J. Parkinson: Permission accounting in separation logic. POPL 2005: 259-270

Peter W. O'Hearn: Scalable Specification and Reasoning: Challenges for Program Logic. VSTTE 2005: 116-133

David J. Pym, Peter W. O'Hearn, Hongseok Yang: Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315(1): 257-305 (2004)

Peter W. O'Hearn: Resources, Concurrency and Local Reasoning. CONCUR 2004: 49-67

Peter W. O'Hearn: Resources, Concurrency, and Local Reasoning (Abstract). ESOP 2004: 1-2

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn: A Decidable Fragment of Separation Logic. FSTTCS 2004: 97-109

Ivana Mijajlovic, Noah Torp-Smith, Peter W. O'Hearn: Refinement and Separation Contexts. FSTTCS 2004: 421-433

Peter W. O'Hearn, Hongseok Yang, John C. Reynolds: Separation and information hiding. POPL 2004: 268-280

Peter W. O'Hearn: On bunched typing. J. Funct. Program. 13(4): 747-796 (2003)

Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat: Program logic and equivalence in the presence of garbage collection. Theor. Comput. Sci. 3(298): 557-581 (2003)

Josh Berdine, Peter W. O'Hearn, Uday S. Reddy, Hayo Thielecke: Linear Continuation-Passing. Higher-Order and Symbolic Computation 15(2-3): 181-208 (2002)

Hongseok Yang, Peter W. O'Hearn: A Semantic Basis for Local Reasoning. FoSSaCS 2002: 402-416

Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. APLAS 2001: 289-300

Peter W. O'Hearn, John C. Reynolds, Hongseok Yang: Local Reasoning about Programs that Alter Data Structures. CSL 2001: 1-19

Cristiano Calcagno, Peter W. O'Hearn: On Garbage and Program Logic. FoSSaCS 2001: 137-151

Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. FSTTCS 2001: 108-119

Samin S. Ishtiaq, Peter W. O'Hearn: BI as an Assertion Language for Mutable Data Structures. POPL 2001: 14-26

Peter W. O'Hearn, John C. Reynolds: From Algol to polymorphic linear lambda-calculus. J. ACM 47(1): 167-223 (2000)

Cristiano Calcagno, Samin S. Ishtiaq, Peter W. O'Hearn: Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292. PPDP 2000: 190-201

Peter W. O'Hearn, David J. Pym: The logic of bunched implications. Bulletin of Symbolic Logic 5(2): 215-244 (1999)

Peter J. Freyd, Peter W. O'Hearn, A. John Power, Makoto Takeyama, R. Street, Robert D. Tennent: Bireflectivity. Theor. Comput. Sci. 228(1-2): 49-76 (1999)

Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent: Syntactic Control of Interference Revisited. Theor. Comput. Sci. 228(1-2): 211-252 (1999)

Peter W. O'Hearn, Uday S. Reddy: Objects, Interference, and the Yoneda Embedding. Theor. Comput. Sci. 228(1-2): 253-282 (1999)

Peter W. O'Hearn: Resource Interpretations, Bunched Implications and the alpha lambda-Calculus. TLCA 1999: 258-279

Peter W. O'Hearn: Polymorphism, objects and abstract types. SIGACT News 29(4): 39-50 (1998)

Yoshiki Kinoshita, Peter W. O'Hearn, John Power, Makoto Takeyama, Robert D. Tennent: An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. TACS 1997: 191-212

Peter W. O'Hearn: Note on Algol and Conservatively Extending Functional Programming. J. Funct. Program. 6(1): 171-180 (1996)

Peter J. Freyd, Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama: Bireflectivity. Electr. Notes Theor. Comput. Sci. 1: 199-213 (1995)

Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama: Syntactic control of interference revisited. Electr. Notes Theor. Comput. Sci. 1: 447-486 (1995)

Peter W. O'Hearn, Uday S. Reddy: Objects, interference and the Yoneda embedding. Electr. Notes Theor. Comput. Sci. 1: 487-514 (1995)

Peter W. O'Hearn, Jon G. Riecke: Kripke Logical Relations and PCF. Inf. Comput. 120(1): 107-116 (1995)

Peter W. O'Hearn, Robert D. Tennent: Parametricity and Local Variables. J. ACM 42(3): 658-709 (1995)

Peter W. O'Hearn, Jon G. Riecke: Fully Abstract Translations and Parametric Polymorphism. ESOP 1994: 454-468

Peter W. O'Hearn, Robert D. Tennent: Semantical Analysis of Specification Logic, 2. Inf. Comput. 107(1): 25-57 (1993)

Peter W. O'Hearn: A Model for Syntactic Control of Interference. Mathematical Structures in Computer Science 3(4): 435-465 (1993)

Peter W. O'Hearn, Robert D. Tennent: Relational Parametricity and Local Variables. POPL 1993: 171-184

Peter W. O'Hearn, Zbigniew Stachniak: Resolution Framework for Finitely-Valued First-Order Logics. J. Symb. Comput. 13(3): 235-254 (1992)

Peter W. O'Hearn: Linear Logic and Interference Control. Category Theory and Computer Science 1991: 74-93

Peter W. O'Hearn, Zbigniew Stachniak: Note on Theorem Proving Strategies for Resolution Counterparts of Non-Classical Logics. ISSAC 1989: 364-372

Peter W. O'Hearn, Zbigniew Stachniak: A Resolution Framework for Finitely-Valued First-Order Logics. SCAI 1989: 69-81