Search for: All records

This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility -- automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program's resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof. 

This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof. 

Women experience higher morbidity than men, despite living longer. This is often attributed to biological differences between the sexes; however, the majority of societies in which these disparities are observed exhibit gender norms that favor men. We tested the hypothesis that female-biased gender norms ameliorate gender disparities in health by comparing gender differences in inflammation and hypertension among the matrilineal and patrilineal Mosuo of China. Widely reported gender disparities in health were reversed among matrilineal Mosuo compared with patrilineal Mosuo, due to substantial improvements in women’s health, with no concomitant detrimental effects on men. These findings offer evidence that gender norms limiting women’s autonomy and biasing inheritance toward men adversely affect the health of women, increasing women’s risk for chronic diseases with tremendous global health impact.