Differential effects of insulin signaling on individual carbon fluxes for fatty acid synthesis in brown adipocytes

Considering the major role of insulin signaling on fatty acid synthesis via stimulation of lipogenic enzymes, differential effects of insulin signaling on individual carbon fluxes for fatty acid synthesis have been investigated by comparing the individual lipogenic fluxes in WT and IRS-1 knockout (IRS-1 KO) brown adipocytes. Results from experiments on WT and IRS-1 KO cells incubated with [5-¹³C] glutamine were consistent with the existence of reductive carboxylation pathway. Analysis of isotopomer distribution of nine metabolites related to the lipogenic routes from glucose and glutamine in IRS-1 KO cells using [U-¹³C] glutamine as compared to that in WT cells indicated that flux through reductive carboxylation pathway was diminished while flux through conventional TCA cycle was stimulated due to absence of insulin signaling in IRS-1 KO cells. This observation was confirmed by quantitative estimation of individual lipogenic fluxes in IRS-1 KO cells and their comparison with fluxes in WT cells. Thus, these results suggest that glutamine’s substantial contribution to fatty acid synthesis can be directly manipulated by controlling the flux through reductive carboxylation of alpha-ketoglutarate to citrate using hormone (insulin).

Type-alpha DPLs

This paper introduces Denotational Proof Languages (DPLs). DPLs are languages for presenting, discovering, and checking formal proofs. In particular, in this paper we discus type-alpha DPLs---a simple class of DPLs for which termination is guaranteed and proof checking can be performed in time linear in the size of the proof. Type-alpha DPLs allow for lucid proof presentation and for efficient proof checking, but not for proof search. Type-omega DPLs allow for search as well as simple presentation and checking, but termination is no longer guaranteed and proof checking may diverge. We do not study type-omega DPLs here. We start by listing some common characteristics of DPLs. We then illustrate with a particularly simple example: a toy type-alpha DPL called PAR, for deducing parities. We present the abstract syntax of PAR, followed by two different kinds of formal semantics: evaluation and denotational. We then relate the two semantics and show how proof checking becomes tantamount to evaluation. We proceed to develop the proof theory of PAR, formulating and studying certain key notions such as observational equivalence that pervade all DPLs. We then present NDL, a type-alpha DPL for classical zero-order natural deduction. Our presentation of NDL mirrors that of PAR, showing how every basic concept that was introduced in PAR resurfaces in NDL. We present sample proofs of several well-known tautologies of propositional logic that demonstrate our thesis that DPL proofs are readable, writable, and concise. Next we contrast DPLs to typed logics based on the Curry-Howard isomorphism, and discuss the distinction between pure and augmented DPLs. Finally we consider the issue of implementing DPLs, presenting an implementation of PAR in SML and one in Athena, and end with some concluding remarks.

Simplifying transformations for type-alpha certificates

This paper presents an algorithm for simplifying NDL deductions. An array of simplifying transformations are rigorously defined. They are shown to be terminating, and to respect the formal semantis of the language. We also show that the transformations never increase the size or complexity of a deduction---in the worst case, they produce deductions of the same size and complexity as the original. We present several examples of proofs containing various types of "detours", and explain how our procedure eliminates them, resulting in smaller and cleaner deductions. All of the given transformations are fully implemented in SML-NJ. The complete code listing is presented, along with explanatory comments. Finally, although the transformations given here are defined for NDL, we point out that they can be applied to any type-alpha DPL that satisfies a few simple conditions.