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.
|Title of host publication||Typed Lambda Calculi and Applications|
|Subtitle of host publication||8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings|
|Publisher||Springer Berlin Heidelberg|
|Number of pages||17|
|Publication status||Published - 2007|