Sciweavers

POPL
2009
ACM

Focusing on pattern matching

14 years 5 months ago
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
Neelakantan R. Krishnaswami
Added 22 Nov 2009
Updated 22 Nov 2009
Type Conference
Year 2009
Where POPL
Authors Neelakantan R. Krishnaswami
Comments (0)