Copenhagen Programming Language Seminar

Completeness for algebraic theories of local state

Sam Staton
Cambridge University

Tuesday, November 24th, 2009, 14:00 - 15:00
IT University, Copenhagen. Room: AuditorÝum 4


What is a theory of equality for first-order programs with local state (allocation, dereferencing, and assignment)?

I will present an algebraic theory with axioms such as (l:=n;!l) == (l:=n;n) and (let l=ref(v) in l:=w;l) == (let l=ref(w) in l). My central result is that the theory is complete, in the following sense: any additional axiom is either derivable already, or introduces inconsistency. So we have all the axioms for local state. (This is sometimes called "Hilbert- Post completeness").

This builds on the work on enriched algebraic theories and generic effects by Plotkin and Power. The question about completeness for local state was first posed in their FOSSACS'02 paper.

Scientific host: Rasmus M°gelberg  Administrative host:RenÚe Korver Michan. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org