BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Focusing on Pattern Matching - Neelakantan Krishnaswami\, CMU
DTSTART:20081027T124500Z
DTEND:20081027T140000Z
UID:TALK14770@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:From the point of view of the semanticist\, one of the chief a
 ttractions of functional programming is the close connection of the typed 
 lambda calculus to proof theory and logic via the Curry-Howard corresponde
 nce. 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 w
 ith pattern matching. But pattern matching\, though enormously useful\, ha
 s historically lacked the close tie to logic that the other core features 
 of functional languages possess.\n\nThe Definition of Standard ML\, for ex
 ample\, contains a suggestion in English that it would be desirable to che
 ck coverage\, with no clear account of what this means or how to accomplis
 h it. In this talk we will argue the semanticist ought to be just as inter
 ested in pattern matching as the programmer. We show that pattern matching
  has a strong logical interpretation via the proof-theoretic notion of foc
 using\, and that filling in this part of the Curry-Howard correspondence e
 nables simple correctness proofs of parts of the compiler (such as the cov
 erage checker and the pattern compiler) that required considerable insight
  and creativity before.\n\n(This work will appear in POPL 2009.)
LOCATION:FW26
END:VEVENT
END:VCALENDAR