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.
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.