Extensional Rewriting with Sums

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.

• Type: Conference
• Year: 2007
• Where: TLCA
• Authors: Sam Lindley
• Keywords: Extensional Equational Theory, Extensional Rewriting Theory, Sum Types, Theoretical Computer Science, TLCA 2007