Abstract

From the point of view of the semanticist, one of the chief attractions of functional programming is the close connection of the typed lambda calculus to proof theory and logic via the Curry-Howard correspondence. The point of view of the workaday programmer seems, at first glance, less exalted – one of the most compelling features in actual programming languages like ML and Haskell is the ability to analyze structured data with pattern matching. But pattern matching, though enormously useful, has historically lacked the close tie to logic that the other core features of functional languages possess.

The Definition of Standard ML, for example, contains a suggestion in English that it would be desirable to check coverage, with no clear account of what this means or how to accomplish it. In this talk we will argue the semanticist ought to be just as interested in pattern matching as the programmer. We show that pattern matching has a strong logical interpretation via the proof-theoretic notion of focusing, and that filling in this part of the Curry-Howard correspondence enables simple correctness proofs of parts of the compiler (such as the coverage checker and the pattern compiler) that required considerable insight and creativity before.

(This work will appear in POPL 2009 .)