BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Completeness for algebraic theories of local state - Sam Staton (C
 omputer Laboratory\, University of Cambridge)
DTSTART:20091116T124500Z
DTEND:20091116T140000Z
UID:TALK20700@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:What is a theory of equality for first-order programs with loc
 al state (allocation\,\ndereferencing\, and assignment)? I will present an
  algebraic theory with\naxioms such as (l:=n\;!l) = (l:=n\;n) and (let l=r
 ef(v) in l:=w\;l) = (let\nl=ref(w) in l). My central result is that the th
 eory is complete\, in the\nfollowing sense: any additional axiom is either
  derivable already\, or introduces\ninconsistency. So we have all the axio
 ms for local state. (This is sometimes\ncalled "Hilbert- Post completeness
 ").\n\nThis builds on the work on enriched algebraic theories and generic 
 effects\nby Plotkin and Power. The question about completeness for local s
 tate was\nfirst posed in their FOSSACS'02 paper.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR