分离逻辑继承与发展了霍尔逻辑，进一步发展了程序推理与验证理论,拓展了程序逻辑理论。 Peter O'Hearn Professor of Computer Science Royal Society Wolfson Research Merit Award Holder Member of Theory Research Group Address: Department of Computer Science , Queen Mary, University of London, London, E1 4NS, UK Phone: +44 (0)20 7882 5443; Fax: +44 (0)20 8980 6533; e-mail: ohearn AT dcs.qmul.ac.uk My research interests are in logic and semantics of computation. With John Reynolds (CMU) I developed separation logic, which addresses the problem of tractable reasoning about dynamically allocated objects. With David Pym (then at Queen Mary, now at HP) I developed bunched logic, a general logic of resource, which is a more abstract cousin of and precursor to separation logic. In recent years I've been tempted into tools research where I help out, or get dragged along by, many excellent colleagues in the London/Cambridge area who are enthusiastically pursuing mechanized program verification and static program analysis. This particularly involves the SpaceInvader team (Cristiano Calcagno, Dino Distefano, Hongseok Yang and me) in London and our SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine, Byron Cook). John C. Reynolds Professor Computer Science Department School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890 9019 Gates Center, 412-268-3057, fax: 412-268-5576 email: John DOT Reynolds AT cs DOT cmu DOT edu assistant: Tracy Farbacher 9129 Gates Center, 412-268-8824 email: tracyf AT cs DOT cmu DOT edu Research Interests My research centers on the design of programming languages and languages for specifying program behavior, mathematical tools for defining the semantics of such languages, and methods for proving that programs meet their specifications. At present, my main goal is to extend the strong-typing and proof systems that characterize higher-level languages to lower-level languages that give the user control over data representation and storage allocation. In particular, I have developed, in joint work with Peter O'Hearn at Queen Mary, University of London, a new logic called separation logic, that facilitates reasoning about shared mutable data structures. A second area of interest is the semantics of types. The last fifteen years have seen the discovery of a variety of type systems that have vastly enlarged our notions of what types are and how they might be used. My goal is to understand the meaning of these systems and to find a general concept of type of which they are all instances. Finally, I am interested in the design, definition, and proof methodology of Algol-like languages, which combine imperative constructs with a powerful procedure mechanism, while retaining the concepts of block structure and local variables. I am a member of the Principles of Programming group here at CMU. I am also a member of the advisory board of the journal Higher-Order and Symbolic Computation .
标签: 分离逻辑（separation
