Extensional Rewriting with Sums

Sam Lindley

Research output: Chapter in Book/Report/Conference proceedingChapter

16 Citations (Scopus)

Abstract

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

Publication series

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

Fingerprint

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

Cite this