If $latex f$ and $latex g$ are functions, what does $latex f*g$ mean? Definition 1. A separation algebra (citation) is a triple $latex (M, \circ, u)$, where $latex M$ is a set, $latex \circ$ has type $latex M \times M \rightharpoonup M$ and is commutative, associative and cancellative, and $latex u\in M$ is the unit… Continue reading A star operator for functions

# Category: Separation Logic

## A comment on ‘Abstract Separation Logic’

Abstract Separation Logic (citation) is based on a partial composition operator, $latex \circ$, which has the following type: $latex \circ : \Sigma \times \Sigma \rightharpoonup \Sigma$ We shall concentrate henceforth on the simplest incarnation of this operator: disjoint union. Here are two useful theorems about disjoint union. Theorem 1. If $latex a\subseteq a'$ and $latex… Continue reading A comment on ‘Abstract Separation Logic’