Completeness for algebraic theories of local state
Add to your list(s)
Download to your calendar using vCal
If you have a question about this talk, please contact Sam Staton.
What is a theory of equality for firstorder 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.
This talk is part of the Semantics Lunch (Computer Laboratory) series.
This talk is included in these lists:
Note that exdirectory lists are not shown.
