B Cell Activation in Insulin Resistance and Obesity

Our group has demonstrated that inflammatory diseases such as type 2 diabetes (DM), inflammatory bowel disease (IBD), and periodontal disease (PD) are associated with altered B cell function that may contribute to disease pathogenesis. B cells were found to be highly activated with characteristics of inflammatory cells. Obesity is a pre-disease state for cardiovascular disease and type 2 diabetes and is considered a state of chronic inflammation. Therefore, we sought to better characterize B cell function and phenotype in obese patients. We demonstrate that (Toll-like receptor) TLR4 and CD36 expression by B cells is elevated in obese subjects, suggesting increased sensing of lipopolysaccharide (LPS) and other TLR ligands. These ligands may be of microbial, from translocation from a leaky gut, or host origin. To better assess microbial ligand burden and host response in the bloodstream, we measured LPS binding protein (LBP), bacterial/permeability increasing protein (BPI), and high mobility group box 1 (HMGB1). Thus far, our data demonstrate an increase in LBP in DM and obesity indicating increased responses to TLR ligands in the blood. Interestingly, B cells responded to certain types of LPS by phosphorylating extracellular-signal-regulated kinases (ERK) 1/2. A better understanding of the immunological state of obesity and the microbial and endogenous TLR ligands that may be activating B cells will help identify novel therapeutics to reduce the risk of more dangerous conditions, such as cardiovascular disease.

Typability and Type Checking in the Second-Order Λ-Calculus Are Equivalent and Undecidable (Preliminary Draft)

We consider the problems of typability[1] and type checking[2] in the Girard/Reynolds second-order polymorphic typed λ-calculus, for which we use the short name "System F" and which we use in the "Curry style" where types are assigned to pure λ -terms. These problems have been considered and proven to be decidable or undecidable for various restrictions and extensions of System F and other related systems, and lower-bound complexity results for System F have been achieved, but they have remained "embarrassing open problems"[3] for System F itself. We first prove that type checking in System F is undecidable by a reduction from semi-unification. We then prove typability in System F is undecidable by a reduction from type checking. Since the reverse reduction is already known, this implies the two problems are equivalent. The second reduction uses a novel method of constructing λ-terms such that in all type derivations, specific bound variables must always be assigned a specific type. Using this technique, we can require that specific subterms must be typable using a specific, fixed type assignment in order for the entire term to be typable at all. Any desired type assignment may be simulated. We develop this method, which we call "constants for free", for both the λK and λI calculi.

A Direct Algorithm for the Type Interference in the Rank 2 Fragment of the Second--Order λ-Calculus

We study the problem of type inference for a family of polymorphic type disciplines containing the power of Core-ML. This family comprises all levels of the stratification of the second-order lambda-calculus by "rank" of types. We show that typability is an undecidable problem at every rank k ≥ 3 of this stratification. While it was already known that typability is decidable at rank ≤ 2, no direct and easy-to-implement algorithm was available. To design such an algorithm, we develop a new notion of reduction and show how to use it to reduce the problem of typability at rank 2 to the problem of acyclic semi-unification. A by-product of our analysis is the publication of a simple solution procedure for acyclic semi-unification.

Principality and Decidable Type Inference for Finite-Rank Intersection Types

Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, if possible. We define an intersection type system which has principal typings and types exactly the strongly normalizable λ-terms. More interestingly, every finite-rank restriction of this system (using Leivant's first notion of rank) has principal typings and also has decidable type inference. This is in contrast to System F where the finite rank restriction for every finite rank at 3 and above has neither principal typings nor decidable type inference. This is also in contrast to earlier presentations of intersection types where the status of these properties is not known for the finite-rank restrictions at 3 and above.Furthermore, the notion of principal typings for our system involves only one operation, substitution, rather than several operations (not all substitution-based) as in earlier presentations of principality for intersection types (of unrestricted rank). A unification-based type inference algorithm is presented using a new form of unification, β-unification.