Rationing Antiretroviral Therapy for HIV/AIDS in Africa: Efficiency, Equity, and Reality

Background: Rationing of access to antiretroviral therapy already exists in sub-Saharan Africa and will intensify as national treatment programs develop. The number of people who are medically eligible for therapy will far exceed the human, infrastructural, and financial resources available, making rationing of public treatment services inevitable. Methods: We identified 15 criteria by which antiretroviral therapy could be rationed in African countries and analyzed the resulting rationing systems across 5 domains: clinical effectiveness, implementation feasibility, cost, economic efficiency, and social equity. Findings: Rationing can be explicit or implicit. Access to treatment can be explicitly targeted to priority subpopulations such as mothers of newborns, skilled workers, students, or poor people. Explicit conditions can also be set that cause differential access, such as residence in a designated geographic area, co-payment, access to testing, or a demonstrated commitment to adhere to therapy. Implicit rationing on the basis of first-come, first-served or queuing will arise when no explicit system is enforced; implicit systems almost always allow a high degree of queue-jumping by the elite. There is a direct tradeoff between economic efficiency and social equity. Interpretation: Rationing is inevitable in most countries for some period of time. Without deliberate social policy decisions, implicit rationing systems that are neither efficient nor equitable will prevail. Governments that make deliberate choices, and then explain and defend those choices to their constituencies, are more likely to achieve a socially desirable outcome from the large investments now being made than are those that allow queuing and queue-jumping to dominate.

System F with Constraint Types

System F is a type system that can be seen as both a proof system for second-order propositional logic and as a polymorphic programming language. In this work we explore several extensions of System F by types which express subtyping constraints. These systems include terms which represent proofs of subtyping relationships between types. Given a proof that one type is a subtype of another, one may use a coercion term constructor to coerce terms from the first type to the second. The ability to manipulate type constraints as first-class entities gives these systems a lot of expressive power, including the ability to encode generalized algebraic data types and intensional type analysis. The main contributions of this work are in the formulation of constraint types and a proof of strong normalization for an extension of System F with constraint types.

Fixed Point vs. First-Order Logic on Finite Ordered Structures with Unary Relations

We prove that first order logic is strictly weaker than fixed point logic over every infinite classes of finite ordered structures with unary relations: Over these classes there is always an inductive unary relation which cannot be defined by a first-order formula, even when every inductive sentence (i.e., closed formula) can be expressed in first-order over this particular class. Our proof first establishes a property valid for every unary relation definable by first-order logic over these classes which is peculiar to classes of ordered structures with unary relations. In a second step we show that this property itself can be expressed in fixed point logic and can be used to construct a non-elementary unary relation.

Securing Bulk Content Almost for Free

Content providers often consider the costs of security to be greater than the losses they might incur without it; many view "casual piracy" as their main concern. Our goal is to provide a low cost defense against such attacks while maintaining rigorous security guarantees. Our defense is integrated with and leverages fast forward error correcting codes, such as Tornado codes, which are widely used to facilitate reliable delivery of rich content. We tune one such family of codes - while preserving their original desirable properties - to guarantee that none of the original content can b e recovered whenever a key subset of encoded packets is missing. Ultimately we encrypt only these key codewords (only 4% of all transmissions), making the security overhead negligible.