Abstract We present a new semantics for Algol-like languages that combines methods from two prior lines of development: ffl the object-based approach of [21,22], where the meaning of an imperative...
Petri Net Semantics of Bunched Implications (2008)
Engberg and Winskel's Petri net semantics of linear logic is re-considered, from the point of view of the logic BI of bunched implications. We first show how BI can be used to overcome a number...
Column Editor Jon, Jon G. Riecke, Peter W. O'hearn
Types Peter W. O'Hearn Department of Computer Science Queen Mary & Westfield College (ohearn@dcs.qmw.ac.uk) October 7, 1998 1 Introduction Abstraction is one of the pillars of computer...
Petri Net Semantics of Bunched Implications (2007)
Peter O'Hearn And Hongseok Yang, Peter W. O'hearn, Hongseok Yang
Engberg and Winskel's Petri net semantics of linear logic is re-considered, from the point of view of the logic BI of bunched implications. We first show how BI can be used to overcome a number...
Petri Net Semantics of Bunched Implications (2007)
Peter W. O'Hearn, Hongseok Yang
Engberg and Winskel's Petri net semantics of linear logic is re-considered, from the point of view of the logic BI of bunched implications. We first show how BI can be used to overcome a number...
Seoul National University (2007)
Peter W. O'hearn, Queen Mary, Hongseok Yang, John C. Reynolds, Carnegie Mellon
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from...
Peter W. O'hearn, Hongseok Yang
Abstract. Engberg and Winskel's Petri net semantics of linear logic is re-considered, from the point of view of the logic BI of bunched implications. We first show how BI can be used to overcome...
Flexible Interference Control with Bunches (2007)
In 1978, John Reynolds introduced Syntactic Control of Interference, a type-based method of managing aliasing and other forms interference resulting from shared storage. In contemporary terms,...
Extracting the Range of cps from Ane Typing Extended Abstract (2007)
Josh Berdine, Peter W. O'hearn, Hayo Thielecke
Increasing degrees of reasoning about programs are being mechanized, and hence more formality is needed. Here we present an instance of this formalization in the form of a precise characterization of...
John C. Reynolds, Peter W. O'hearn, Heap Faults
Extention of Hoare logic for imperative programs Store/heap dichotomy Heap-manipulation commands (not expressions) Independent conjuction ( )
Peter W. O'hearn, Hongseok Yang
Abstract. Engberg and Winskel's Petri net semantics of linear logic is re-considered, from the point of view of the logic BI of bunched implications. We rst show how BI can be used to overcome a...
John C. Reynolds, Peter W. O'hearn, Hongseok Yang
The topic of these lectures is an extension of Hoare logic [1, 2] to the specication and proof of programs in which data structures can contain several pointers to the same location, whose contents...
John C. Reynolds, Peter W. O'hearn
ffl Extention of Hoare logic for imperative programs ffl Store/heap dichotomy ffl Heap-manipulation commands (not expressions) ffl Independent conjunction ( ) ffl Unrestricted address arithmetic ffl...
Cristiano Calcagno, Samin Ishtiaq, Peter W. O'hearn, Queen Mary, Queen Mary
Bornat has recently described an approach to reasoning about pointers, building on work of Morris. Here we describe a semantics that validates the approach, and use it to help devise axioms for...
On Ane Typing and Completeness of cps Extended Summary Draft (2007)
Josh Berdine, Peter W. O'hearn, Hayo Thielecke
This paper is a companion to \Linearly Used Continuations " by the authors. There, we show how a variety of control behaviours use continuations anely, including calling/returning...
A Local Shape Analysis based on Separation Logic (2006)
Dino Distefano, Peter W. O'Hearn, Peter W. O’hearn, Hongseok Yang
We describe a program analysis for linked list programs where the abstract domain uses formulae from separation logic.
Symbolic Execution with Separation Logic (2005)
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn, Peter W. O’hearn, Queen Mary
We describe a sound method for automatically proving Hoare triples for loop-free code in Separation Logic, for certain preconditions and postconditions (symbolic heaps). The method uses a form of...
Resources, Concurrency and Local Reasoning (2005)
Peter W. O'Hearn, Peter W. O’hearn, Queen Mary, To John, C. Reynolds
In this paper we show how a resource-oriented logic, separation logic, can be used to reason about the usage of resources in concurrent programs.
Separation and Information Hiding (2004)
Peter W. O'Hearn, Hongseok Yang, John C. Reynolds, Peter W. O’hearn, Queen Mary
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from...
Possible worlds and resources: The semantics of BI (2003)
David J. Pym, Peter W. O'hearn, Hongseok Yang
The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining...
Possible worlds and resources: The semantics of BI (2003)
David J. Pym, Peter W. O'hearn, Hongseok Yang
The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining...
Possible worlds and resources: The semantics of BI (2003)
David J. Pym, Peter W. O'hearn, Hongseok Yang
The logic of bunched implications, BI, is a substructural system which freely combines an additive (intuitionistic) and a multiplicative (linear) implication via bunches (contexts with two combining...
Computability and complexity results for a spatial assertion language for data structures (2001)
Cristiano Calcagno, Hongseok Yang, Peter W. O'hearn
Abstract. This paper studies a recently developed an approach to reasoning about mutable data structures, which uses an assertion language with spatial conjunction and implication connectives. We...
Computability and complexity results for a spatial assertion language for data structures (2001)
Cristiano Calcagno, Hongseok Yang, Peter W. O'hearn
Abstract. This paper studies a recently developed an approach to reasoning about mutable data structures, which uses an assertion language with spatial conjunction and implication connectives. We...
On garbage and program logic (2001)
Cristiano Calcagno, Peter W. O'hearn
Abstract. Garbage collection relieves the programmer of the burden of managing dynamically allocated memory, by providing an automatic way to reclaim unneeded storage. This eliminates or lessens...
Computability and complexity results for a spatial assertion language for data structures (2001)
Cristiano Calcagno, Hongseok Yang, Peter W. O'hearn
Abstract. Reynolds, Ishtiaq and O'Hearn have recently developed an approach to reasoning about mutable data structures using an assertion language with spatial conjunction and implication...
Linearly used continuations (2001)
Josh Berdine, Peter W. O'hearn, Uday S. Reddy, Hayo Thielecke
Continuations are the raw material of control. They can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling
BI as an assertion language for mutable data structures (2001)
Samin Ishtiaq, Peter W. O'hearn
Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We...
On garbage and program logic (2001)
Cristiano Calcagno, Peter W. O'hearn
Abstract. Memory safe programming languages harness the power of pointers by disallowing certain operations { notably operations for pointer arithmetic and disposal { and memory reclamation is often...
On garbage and program logic (2001)
Peter W. O'hearn, Cristiano Calcagno
Abstract. Memory-safe programming languages harness the power of pointers by disallowing certain operations { notably operations for pointer arithmetic and disposal { and memory reclamation is often...
Linearly used continuations (2001)
Josh Berdine, Peter W. O'hearn, Uday S. Reddy, Hayo Thielecke
Continuations are the raw material of control. They can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling
Computability and Complexity Results for a Spatial Assertion Language for Data Structures (2001)
Cristiano Calcagno, Hongseok Yang, Peter W. O'Hearn, Peter W. O’hearn, Queen Mary
This paper studies a recently developed an approach to reasoning about mutable data structures, which uses an assertion language with spatial conjunction and implication connectives. We investigate...
On garbage and program logic (2001)
Cristiano Calcagno, Peter W. O'hearn
1 Introduction Garbage collection is an essential method used to reclaim heap-allocated objects whose lifetime cannot be easily predicted at compile time. It is most strongly associated with...
as an assertion language for mutable data structures (2001)
Samin Ishtiaq, Peter W. O'hearn, Queen Mary, Westfield College
Pointers are an extremely powerful and flexible programming mechanism, useful for manipulating linked data structures and for providing structured access to data in memory. They are also extremely...
Possible Worlds and Resources: The Semantics of BI (2000)
Peter W. O'Hearn, David J. Pym, Hongseok Yang
In a previous paper, O'Hearn and Pym introduced a new substructural logic, the logic BI of bunched implications. Herein, motivated by modelling resources, we investigate the possible worlds...
Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic (2000)
Cristiano Calcagno, Samin Ishtiaq, Peter W. O'Hearn
Bornat has recently described an approach to reasoning about pointers, building on work of Morris. Here we describe a semantics that validates the approach, and use it to help devise axioms for...
BI as an Assertion Language for Mutable Data Structures (2000)
Samin Ishtiaq, Peter W. O'Hearn
Reynolds has recently developed a logic for reasoning about mutable data structures, where pre- and post-conditions are written in an intuitionistic logic enriched with a spatial form of conjunction....
The Logic of Bunched Implications (1999)
Abstract. We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of...
The Logic of Bunched Implications (1999)
Peter W. O'Hearn, David J. Pym
We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the...
Resource Interpretations, Bunched Implications and the alphalambda-calculus (1999)
. We introduce the ff-calculus, a typed calculus that includes a multiplicative function type \Gamma alongside an additive function type !. It arises proof-theoretically as a calculus of proof terms...
From Algol to Polymorphic Linear Lambda-calculus (1997)
Peter W. O'Hearn, Queen Mary, John C. Reynolds
ion and Store Shapes . . . . . . . . . . 6 2 Two Variations on Algol 8 2.1 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Name: P.W. O'Hearn Address: Department of...
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement (1997)
Yoshiki Kinoshita, Peter W. O'hearn, A. John Power, Makoto Takeyama, Robert D. Tennent
We introduce an axiomatic approach to logical relations and data refinement. We consider a programming language and the monad on the category of small categories generated by it. We identify abstract...
An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement (1997)
Yoshiki Kinoshita, Peter W. O'Hearn, A. John Power, Makoto Takeyama, Robert D. Tennent
We introduce an axiomatic approach to logical relations and data refinement. We consider a programming language and the monad on the category of small categories generated by it. We identify abstract...
From Algol to Polymorphic Linear Lambda-calculus (1996)
Peter W. O'Hearn, John C. Reynolds
We translate two variations on Algol 60 into the polymorphic linear lambda-calculus, extended with a fixed-point operator. One of the translations is for a version of Idealized Algol with side...
Objects, Interference, and the Yoneda Embedding (1995)
Peter W. O'Hearn, Uday S. Reddy
We present a new semantics for Algol-like languages that combines methods from two prior lines of development: ffl the object-based approach of [28,29], where the meaning of an imperative program is...
Kripke Logical Relations and PCF (1995)
Peter W. O'Hearn, Jon G. Riecke
Sieber has described a model of PCF consisting of continuous functions that are invariant under certain (finitary) logical relations, and shown that it is fully abstract for closed terms of up to...