Focusing on Pattern Matching

Add to your list(s) Download to your calendar using vCal

• Neelakantan Krishnaswami, CMU
• Monday 27 October 2008, 12:45-14:00
• FW26.

If you have a question about this talk, please contact Matthew Parkinson.

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

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.