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) > Abstract separation algebra

## Abstract separation algebraAdd to your list(s) Download to your calendar using vCal - Tony Hoare (Microsoft Research)
- Monday 04 October 2010, 12:45-14:00
- Room FW26, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Sam Staton. I show how both Hoare triples and Plotkin triples can be replaced by an abstract algebra, in which all the primitives are pairs and singletons, i.e., constants, binary operators and binary predicates. The algebra deals separately but equally simply with both sequential and concurrent composition of programs; and many further program primitives and structuring operators like choice and disjoint concurrency can be introduced individually, one at a time. The relevant proof rules for Hoare Triples, and the relevant Plotkin triples for operational semantics, are derived simply and separately for each binary operator. Familiar algebraic properties – associativity, commutivity, monotonicity, idempotence are widely reused. The interactions between operators can be described just two at a time by distributivity laws. These include mutual distribution, a weak form of the exchange law of two-category theory. This leads to an elementary presentation of separation logic and of Kleene algebra. Thus we extend to the mathematics of programming the old saying about marriage: ‘two’s fun, three’s none’. Down with the triple! 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 listsDarwin Society (Christ's) Philomathia Social Sciences Research Programme CIMR Professional Development Seminars## Other talksThe Object of My Affection: stories of love from the Fitzwilliam collection MicroRNAs as circulating biomarkers in cancer Eukaryotic cell division and its origins The Hopkins Lecture 2018 - mTOR and Lysosomes in Growth Control The role of Birkeland currents in the Dungey cycle Microsporidia: diverse, opportunistic and pervasive pathogens |