Bob Harper, Self-Adjusting Computation
Abstract: A static algorithm is one that computes the result of a query about the output for a single, fixed input. For example, a static sorting algorithm is one that takes as input a set of keys, and permits queries about the relative order of these keys according to some ordering relation. A dynamic, or incremental, algorithm is one that permits queries about the output to be interleaved with operations that incrementally modify the input. For example, a dynamic sorting algorithm is one that would permit insertion or deletion of keys to be interleaved with queries about their relative ordering. Self-adjusting computation is a method for deriving a dynamic algorithm from a static algorithm by applying three main techniques: adaptivity, which permits the output of an algorithm to be adjusted to reflect changes to its input; selective memoization, which permits re-use of results based on accurate control flow information rather than simple call patterns; and adaptive memoization, which permits re-use of incorrect computations by adaptation. These techniques are realized as linguistic mechanisms in a statically typed functional language whose type system guarantees that the effects of an input modification are correctly propagated to their outputs, thereby ensuring that the dynamic algorithm is correct relative to its static counterpart. Using these methods we obtain dynamic versions of several well-known algorithms, including a dynamic version of Quicksort that adapts to insertions and deletions in expected logarithmic time.
Bio: Robert Harper received the Ph.D. in Computer Science from Cornell University in 1985. His thesis work was concerned with the design and implementation of the NuPRL proof development environment. From 1985 to 1988 he was a research fellow at the Laboratory for Foundations of Computer Science at Edinburgh University, Edinburgh, Scotland. Dr. Harper was a member of the Standard ML design team, developed the first implementation of the SML modules system, and co-authored the formal semantics of Standard ML. He, together with Gordon Plotkin and Furio Honsell, invented the LF logical framework, a general language for describing and implementing formal logical systems.
Dr. Harper joined the faculty of the School of Computer Science at at Carnegie Mellon University in 1988, where he is currently a Professor of Computer Science. Dr. Harper was a co-Principal Investigator on the Fox Project on Advanced Languages for Systems Software and the PSciCo Project on Parallel Scientific Computing. He is currently co-Principal Investigator on the ConCert Project on Trustless Grid Computing and the Triple Project on Type Refinementsfor Programming Languages. His primary research interests are in the application of type theory to the design, semantics, and implementation of advanced programming languages.