![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Sam Staton (Computer Laboratory, University of Cambridge)
Monday 16 November 2009, 12:45-14:00
Completeness for algebraic theories of local state
- đ¤ Speaker: Sam Staton (Computer Laboratory, University of Cambridge)
- đ Date & Time: Monday 16 November 2009, 12:45 - 14:00
- đ Venue: Room FW26, Computer Laboratory, William Gates Building
Abstract
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.
Series This talk is part of the Semantics Lunch (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Martin's interesting talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.