An update calculus for expressing type-safe program updates