University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > Completeness for algebraic theories of local state

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 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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity