TY - CHAP

T1 - Extensional Rewriting with Sums

AU - Lindley, Sam

PY - 2007

Y1 - 2007

N2 - Inspired by recent work on normalisation by evaluation for sums, we propose a normalising and confluent extensional rewriting theory for the simply-typed λ-calculus extended with sum types. As a corollary of confluence we obtain decidability for the extensional equational theory of simply-typed λ-calculus extended with sum types. Unlike previous decidability results, which rely on advanced rewriting techniques or advanced category theory, we only use standard techniques.

AB - Inspired by recent work on normalisation by evaluation for sums, we propose a normalising and confluent extensional rewriting theory for the simply-typed λ-calculus extended with sum types. As a corollary of confluence we obtain decidability for the extensional equational theory of simply-typed λ-calculus extended with sum types. Unlike previous decidability results, which rely on advanced rewriting techniques or advanced category theory, we only use standard techniques.

U2 - 10.1007/978-3-540-73228-0_19

DO - 10.1007/978-3-540-73228-0_19

M3 - Chapter

SN - 9783540732273

T3 - Lecture Notes in Computer Science

SP - 255

EP - 271

BT - Typed Lambda Calculi and Applications

PB - Springer

ER -