I think perhaps this could be done in other ways that don't require interval arithmetic for autodiff, only that the gradient is conservatively computed, in other words carrying the numerical error from f into f'
1) compute f with interval arithmetic
2) compute f normally and f' with interval arithmetic
3) compute f rounding towards zero, compute f' from f rounded towards infinity, and round f' up (if f positive) or round f' down (if f negative).
In all 3 cases you can use what you computed to figure out bounds on f, (1) is direct, the other two need extra work.