Extensional Rewriting with Sums

Sam Lindley

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

Extensional Rewriting with Sums

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

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	8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings
Publisher	Springer Berlin Heidelberg
Pages	255-271
Number of pages	17
Volume	4583
ISBN (Electronic)	978-3-540-73228-0
ISBN (Print)	978-3-540-73227-3
DOIs	https://doi.org/10.1007/978-3-540-73228-0_19
Publication status	Published - 2007

Access to Document

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

Lindley 2007 Extensional rewriting with sumsSubmitted manuscript, 210 KB

http://dx.doi.org/10.1007/978-3-540-73228-0_19

Cite this

@inproceedings{0e1dbeb8fe8a4c73bfc149f803d5dca2,

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 = "978-3-540-73227-3",

volume = "4583",

pages = "255--271",

booktitle = "Typed Lambda Calculi and Applications",

publisher = "Springer Berlin Heidelberg",

}

TY - GEN

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 - Conference contribution

SN - 978-3-540-73227-3

VL - 4583

SP - 255

EP - 271

BT - Typed Lambda Calculi and Applications

PB - Springer Berlin Heidelberg

ER -

Extensional Rewriting with Sums

Abstract

Access to Document

Fingerprint

Cite this