Proof-directed debugging

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 inspire... View More