Extensional Rewriting with Sums

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications
Subtitle of host publication8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages17
ISBN (Electronic)978-3-540-73228-0
ISBN (Print)978-3-540-73227-3
Publication statusPublished - 2007


Dive into the research topics of 'Extensional Rewriting with Sums'. Together they form a unique fingerprint.

Cite this