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 -