Extensional Rewriting with Sums

Sam Lindley

Research output: Chapter in Book/Report/Conference proceedingChapter

10 Citations (Scopus)


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 publicationTLCA 2007
Number of pages17
ISBN (Electronic)9783540732280
ISBN (Print)9783540732273
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


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

Cite this