|||
Professor of Computer ScienceMy 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).
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
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 |
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.
Archiver|手机版|科学网 ( 京ICP备07017567号-12 )
GMT+8, 2024-9-20 21:39
Powered by ScienceNet.cn
Copyright © 2007- 中国科学报社