##
Proof-Directed Debugging

Robert W. Harper

School of Computer Science

Carnegie Mellon University

rwh@cs.cmu.edu
### ABSTRACT

The close relationship between writing programs and proving theorems has
frequently been cited as an advantage of functional programming languages.
We illustrate the interplay between programming and proving in the
development of a program for regular expression matching. The presentation
is inspired by Lakatos's method of proofs and refutations in which the
attempt to prove a plausible conjecture leads to a revision not only of the
proof, but of the theorem itself. We give a plausible implementation of a
regular expression matcher that contains a flaw that is uncovered in an
attempt to prove its correctness. The failure of the proof suggests a
revision of the specification, rather than a change to the code. We then
show that a program meeting the revised specification is nevertheless
sufficient to solve the original problem.

### About the Speaker

Robert Harper was graduated from Rochester Institute of Technology in
1980, and received his Ph.D. in Computer Science from Cornell University in
1985. His thesis work, conducted under the supervision of Robert Constable,
was concerned with the design and implementation of the NuPRL type theory.
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. In addition to his work on SML he also developed the LF
logical framework in conjunction with Gordon Plotkin and Furio Honsell.

Dr. Harper joined the faculty of the School of Computer Science at at Carnegie
Mellon University in 1988, and is currently a tenured Associate Professor of
Computer Science. Together with Peter Lee and Frank Pfenning, he leads the
Fox Project, which is concerned with the development and application of
advanced programming languages. He also leads the PSciCo Project, which is
investigating the use of parallel functional languages for scientific
computing, along with Guy Blelloch, Peter Lee, and Gary Miller. His research
interests are concerned with the application of type theory to the design and
implementation of programming languages, and to the application of programming
language theory to software development.

Colloquia Series page.