分离逻辑继承与发展了霍尔逻辑，进一步发展了程序推理与验证理论,拓展了程序逻辑理论。

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.

转载本文请联系原作者获取授权，同时请注明本文来自黄富强科学网博客。
链接地址：https://blog.sciencenet.cn/blog-89075-285120.html

上一篇：2010计算机科学创新研讨会在清华举行20100106
下一篇：耶鲁大学邵中教授20100108