Logical Reasoning for Higher-Order Functions with Local State