Focusing on pattern matching

In this paper, we show how pattern matching can be seen to arise from a proof term assignment for the focused sequent calculus. This use of the Curry-Howard correspondence allows us to give a novel coverage checking algorithm, and makes it possible to give a rigorous correctness proof for the classical pattern compilation strategy of building decision trees via matrices of patterns. Categories and Subject Descriptors F.4.1 [Mathematical Logic]: Lambda Calculus and Related Systems Keywords Focusing, Pattern Matching, Type Theory, CurryHoward

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Neelakantan R. Krishnaswami
• Keywords: Pattern Compilation Strategy, Pattern Matching, POPL 2009, Programming Languages, Rigorous Correctness Proof