Craig interpolation has become a versatile tool in formal
verification, for instance to generate intermediate assertions for
safety analysis of programs. Interpolants are typically determined by
annotating the steps of an unsatisfiability proof with partial
interpolants. In this paper, we consider Craig interpolation for full
quantifier-free Presburger arithmetic (QFPA), for which currently no
efficient interpolation procedures are known. Closing this gap, we
introduce an interpolating sequent calculus for QFPA and prove it to
be sound and complete. We have extended the Princess theorem prover to
generate interpolating proofs, and applied it to a large number of
publicly available linear integer arithmetic benchmarks. The results
indicate the robustness and efficiency of our proof-based
interpolation procedure.