Extensional Rewriting with Sums

Sam Lindley

doi:10.1007/978-3-540-73228-0_19

Extensional Rewriting with Sums

Sam Lindley

Research output: Chapter in Book/Report/Conference proceeding › Chapter

8 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 language	English
Title of host publication	Typed Lambda Calculi and Applications
Subtitle of host publication	TLCA 2007
Publisher	Springer
Pages	255-271
Number of pages	17
ISBN (Electronic)	9783540732280
ISBN (Print)	9783540732273
DOIs	https://doi.org/10.1007/978-3-540-73228-0_19
Publication status	Published - 2007

Publication series

Name	Lecture Notes in Computer Science
Volume	4583
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-540-73228-0_19

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

Cite this

@inbook{83f26a9c297047208963a95a42538c00,

title = "Extensional Rewriting with Sums",

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.",

author = "Sam Lindley",

year = "2007",

doi = "10.1007/978-3-540-73228-0_19",

language = "English",

isbn = "9783540732273",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "255--271",

booktitle = "Typed Lambda Calculi and Applications",

}

TY - CHAP

T1 - Extensional Rewriting with Sums

AU - Lindley, Sam

PY - 2007

Y1 - 2007

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-540-73228-0_19

DO - 10.1007/978-3-540-73228-0_19

M3 - Chapter

SN - 9783540732273

T3 - Lecture Notes in Computer Science

SP - 255

EP - 271

BT - Typed Lambda Calculi and Applications

PB - Springer

ER -