Semi-Automatic Verification of Purely Functional Programs