We first introduce a very simple typed language for expressing allocation algorithms that allows automatic verification that an algorithm is monotonic and therefore truthful. The analysis of truthfulness is accomplished ...