Focusing on pattern matching
Focusing on pattern matching
复制标题
专注于模式匹配
DOI：
10.1145/1480881.1480927
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
N. Krishnaswami
中科院分区：
文献类型：
--
作者：
N. Krishnaswami
在本文中，我们将展示如何模式匹配可以被看作是产生于一个证明项分配的重点微积分。Curry-Howard对应的使用使我们能够给出一个新的覆盖检查算法，并使得通过模式矩阵构建决策树的经典模式编译策略能够给出严格的正确性证明。
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.