Computer Science Department
School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3890
email: John DOT Reynolds AT cs DOT cmu DOT edu
9129 Gates Center, 412-268-8824
email: tracyf AT cs DOT cmu DOT edu
|
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.
Recently, Bob Tennent extended my macros for
category-theory diagrams ("diagmac" in the above-mentioned ftp files), by using
the pict2e package to permit arbitrary slopes for arrows. He has made this
package, called "diagmac2", available from the
CTAN website.
Making Program Logics Intelligible*
The BCS (British Computer Society)
Lovelace Lecture, London, June 8, 2011
(video,
scrollable slides in pdf,
or overlapping slides in pdf).
In this lecture, I attempt to revive some old concepts and notations for
annotating array-manipulating programs, and to adapt them to separation
logic. The moral of the story is that program logics can be more succinct
and readable than predicate calculus.
Automatic Computation of Static Variable Permissions*
Slides for a talk at MFPS, Pittsburgh,
May 28, 2011 (in pdf). This is work extending
ideas described by U. S. Reddy in an earlier talk at the same conference.
The slides are a preliminary draft, and may not be intelligible without
commentary.
Current Courses at CMU (Spring 2011)
(Including complete videos of the lectures)
CS 818A3 Introduction to Separation Logic (minicourse)*
CS 818A4 Current Research on Separation Logic (minicourse)*
These classes of assertions, which are defined semantically, play a special role in several aspects of separation logic. They allow one to use a full distributive law between ordinary and separating conjunction. They suffice for the soundness of the hypothetical frame rule and O'Hearn's rules for shared-variable concurrency with conditional critical regions. Precise assertions also indicate the absence of memory leaks.
Conventional semantics for shared-variable concurrency suffers from the "grain of time" problem, i.e., the necessity of specifying a default level of atomicity. We propose a semantics that avoids any such choice by regarding all interference that is not controlled by explicit critical regions as catastrophic. It is based on three principles:
When domains are used to model parametric polymorphism, the principle of parametricity (roughly speaking, that polymorphic functions "behave" the same way for all types) permits one to determine many polymorphic domains explicitly. We will explore some interesting examples, including the paradoxical type that cannot be modelled in a set-theoretic semantics.
This is a preprint of a paper in the Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, held July 22-25, 2002 in Copenhagen, Denmark. Copyright 2002 IEEE.
In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.
The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a ``separating conjunction'' that asserts that its subformulas hold for disjoint parts of the heap, and a closely related ``separating implication''. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.
In this paper, we will survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We will also discuss promising future directions.
Spring 2010 CS 812 Programming Language Semantics (starred course)
Spring 2009 CS 818A3 Introduction to Separation Logic (minicourse)*
Spring 2009 CS 818A4 Current Research on Separation Logic (minicourse)*
Spring 2008 CS 812 Programming Language Semantics (starred course)
Spring 2007 CS 818A3 Introduction to Separation Logic (minicourse)*
Spring 2007 CS 818A4 Current Research on Separation Logic (minicourse)*
Spring 2006 CS 812 Programming Language Semantics (starred course)
Spring 2005: CS 818A3 Introduction to Separation Logic (minicourse)*
Spring 2005: CS 818A4 Current Research on Separation Logic (minicourse)*
Spring 2004: CS 819B Specification, Verification, and Model Checking ("Spec and Check") with Ed Clarke
Spring 2004: CS 818A4 Separation Logic (minicourse)*
Fall 2003 (University of Aarhus): Separation Logic (7 lectures)*
Spring 2003: CS 819A3 Specification, Verification, and Refinement of Software (minicourse)
Spring 2003: CS 819A4 Separation Logic (minicourse)*
Spring 2002: CS 819C Reasoning about Low-Level Programming Languages
Spring 2001: CS 819A - Two Minicourses
Spring 2000: CS 819A - Denotational Semantics of Types
Spring 1999: CS 819 - Higher-Order Typed Low-Level Languages
*This material is based upon work partially supported by the National Science Foundation under Grants No. CCR-0204242, CCR-0541021, and CCF-0916808. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.
John DOT Reynolds AT cs DOT cmu
DOT edu
last updated October 2011