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.

Research Papers, Bibliography, and Latex Macros

All of my papers that are available in electronic form, along with a large bibliographic data base and some LATEX macros for category-theory diagrams and various mathematical notations, are available by clicking here to link directly to the ftp files. If you are unable to download thse files click here.

Latex Macros for Category-Theory Diagrams

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)*

Frank Oles' Ph.D. Thesis

Frank Oles has kindly permitted noncommercial distribution of his 1982 thesis "A Category-Theoretic Approach to the Semantics of Programming Languages" (in pdf)

Birthday Greetings to Bob Tennent

Towards a Grainless Semantics for Shared Variable Concurrency*

Slides for an talk at the IT-University, Copenhagen, December 14, 2010 (in pdf). Earlier versions of these slides were used at the FACS (Formal Aspects of Computer Systems) meeting in London, December 6, and a colloquium at Imperial College, December 10. They are a preliminary draft describing work in progress, intended for viewers who heard the talks, and may not be intelligible to others. I intend to update them in the near future.

Readable Proofs in Hoare Logic (and Separation logic)*

Slides for an invited talk at ETAPS2009, York, England, March 25, 2009 (in postscript or pdf). These slides supercede those for the talk "Readable Formal Proofs", given in Toronto on October 6, 2008.

Introduction to Separation Logic*

Lecture Notes for the FIRST PhD Fall School on Logics and Semantics of State, Copenhagen, October 2008 (an expansion of earlier lecture notes for the Marktoberdorf International Summer School, August 2008) (in postscript or pdf).

Some Thoughts on Teaching Programming and Programming Languages

White Paper for the Proceedings of the First SIGPLAN Workshop on Undergraduate Programming Language Curricula (PLC 2008) (in postscript or pdf).

A Toast to Gordon Plotkin

On the occasion of his sixtieth birthday

Grainless Semantics without Critical Regions*

Slides for a talk at MFPS, April 11, 2007, corrected April 27, 2007 (in postscript or pdf).

An Introduction to Separation Logic*

These are the slides for a short course given at EWSCS'06 (The Eleventh Estonian Winter School in Computer Science, Palmse, Estonia, March 5--10, 2006. (in postscript)

Precise, Intuitionistic, and Supported Assertions in Separation Logic*

These are the slides for an invited talk given at MFPS XXI in Birmingham, England on May 21, 2005. (in postscript)

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.

Towards a Grainless Semantics for Shared Variable Concurrency*

Here is a preprint of an invited paper (in postscript or pdf) to be given at FTSTCS 2004 in Chennai, India, December 16, 2004 (copyright Springer-Verlag). (See also Springer's LNCS series homepage.) This supercedes the talk of the same title that I gave at POPL'04.

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:

  • Operations have duration and can overlap one another during execution.
  • If two overlapping operations touch the same location, the meaning of the program execution is "wrong".
  • If, from a given starting state, execution of a program can give "wrong", then no other possibilities need be considered.

Types, Abstraction, and Parametric Polymorphism - for Domains*

Here are the slides (in postscript) of a talk at MFPS XX (May 2004).

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.

A Survey Paper

Separation Logic: A Logic for Shared Mutable Data Structures* (postscript file) (pdf file)

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.

A Book

Theories of Programming Languages, Cambridge University Press, Fall 1998 (hardback), Spring 2009 (paperback)

An Old Book

The Craft of Programming, formerly published by Prentice-Hall International, 1981.

Previous Courses and Lectures

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

Earlier lectures

Students

Professional Vita

(in pdf: short version, long version)

*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