JOHN REYNOLDS
Professor, Computer Science
www

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 for proving that programs meet their specifications.

At present my main goal is to investigate separation logic, a new approach to specifying and verifying programs that alter shared data structures, based upon the ability to assert that properties hold for disjoint areas of storage.

A second area of interest is the semantics of types.  The last quarter-century has 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.