COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Completeness for algebraic theories of local stateAdd to your list(s) Download to your calendar using vCal - Sam Staton (Computer Laboratory, University of Cambridge)
- Monday 16 November 2009, 12:45-14:00
- Room FW26, Computer Laboratory, William Gates Building.
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. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory talks
- Interested Talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsSt Edmund's College Political Forum SECPF Scott Polar Research Institute - Physical Sciences Seminar Science meets Faith## Other talksPrices of peers: identifying endogenous price effects between real assets Structurally unravelling ATP synthase Acceleration of tropical cyclogenesis by self-aggregation feedbacks Deterministic RBF Surrogate Methods for Uncertainty Quantification, Global Optimization and Parallel HPC Applications A unifying theory of branching morphogenesis A compositional approach to scalable statistical modelling and computation |