BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Extensional rewriting with sums - Sam Lindley\, University of Edin
 burgh
DTSTART:20080516T130000Z
DTEND:20080516T140000Z
UID:TALK11115@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Inspired by recent work on normalisation by evaluation for sum
 s\, we propose a normalising and confluent extensional rewriting theory fo
 r the simply-typed lambda-calculus extended with sum types. As a corollary
  of confluence we obtain decidability for the extensional equational theor
 y of simply-typed lambda-calculus extended with sum types. Unlike previous
  decidability results\, which rely on advanced rewriting techniques or adv
 anced category theory\, we only use standard techniques.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR