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.

Eficácia de Spinosad e IGR Plus no controle das pragas de grãos armazenados Rhyzopertha dominica e Sitophilus zeamais.

2008

Cálculo analítico de parâmetros estruturais de proteínas usando a teoria Alpha Shapes.

2007

Exploitation of Ebola Virus VP35 Protein to identify new drugs counteracting its type I IFN antagonism

Ebolaviruses (EBOVs) are among the most virulent and deadly pathogens ever known, causing fulminant haemorrhagic fevers in humans and non-human primates. The 2014 outbreak of Ebola virus disease (EVD) in West Africa has claimed more lives than all previous EVD outbreaks combined. The EBOV high mortality rates have been related to the virus-induced impairment of the host innate immunity reaction due to two virus-coded proteins, VP24 and VP35. EBOV VP35 is a multifunctional protein, it is essential for viral replication as a component of the viral RNA polymerase and it also participates in nucleocapsid assembly. Early during EBOV infection, alpha-beta interferon (IFN-α/β) production would be triggered upon recognition of viral dsRNA products by cytoplasmic retinoic acid-inducible gene I (RIG-I)-like receptors (RLRs). However, this recognition is efficiently prevented by the double-stranded RNA (dsRNA) binding activity of the EBOV VP35 protein, which hides RLRs binding sites on the dsRNA phosphate backbone as well the 5’-triphosphate (5’-ppp) dsRNA ends to RIG-I recognition. In addition to dsRNA binding and sequestration, EBOV VP35 inhibits IFN-α/β production preventing the activation of the IFN regulatory factor 3 (IRF-3) by direct interaction with cellular proteins. Previous studies demonstrated that single amino acid changes in the VP35 dsRNA binding domain reduce EBOV virulence, indicating that VP35 is an attractive target for antiviral drugs development. Within this context, here we report the establishment of a novel method to characterize the EBOV VP35 inhibitory function of the dsRNA-dependent RIG-I-mediated IFN-β signaling pathway in a BLS2 cell culture setting. In such system, a plasmid containing the promoter region of IFN-β gene linked with a luciferase reporter gene was transfected, together with a EBOV VP35 mammalian expression plasmid, into the IFN-sensitive A549 cell line, and the IFN-induction was stimulated through dsRNA transfection. Through alanine scanning mutational studies with biochemical, cellular and computational methods we highlighted the importance of some VP35 residues involved in dsRNA end-capping binding, such as R312, K282 and R322, that may serve as target for the development of small-molecule inhibitors against EBOV. Furthermore, we identified a synthetic compound that increased IFN-induction only under antiviral response stimulation and subverted VP35 inhibition, proving to be very attractive for the development of an antiviral drug. In conclusion, our results provide the establishment of a new assay as a straightforward tool for the screening of antiviral compounds that target i) dsRNA-VP35 or cellular protein-VP35 interaction and ii) dsRNA-dependent RIG-I-mediated IFN signaling pathway, in order to potentiate the IFN response against VP35 inhibition, setting the bases for further drug development.

A Catalogue of the Alpha Chapter Boston University Graduates of the School of Theology 1850-1905

A listing of graduate of Boston University School of Theology and predecessor school. Arranged by class year, alphabetical by last name and geographically by region.

Synthesis and reactivity of alpha-thio-beta-chloroacrylamides and alpha-thio-beta-chloroenones

Development of novel synthetic methodology for selective transformation of organic compounds is a central element underpinning organic synthesis with control of chemo-, regio- and stereoselectivity a very high priority. Reactions which can be conducted under mild reaction conditions and, ideally in an environmentally attractive manner, are particularly advantageous. The principal objective of this thesis was to explore the synthesis, reactivity and synthetic utility of a series of α,β-thio-β-chloroenones. The stereochemical features of these transformations and the potential of this novel series of compounds in the synthesis of bioactive compounds were of particular interest. In exploring the reactivity of these compounds, the key transformations included nucleophilic additions and Stille cross-coupling at the β-carbon. Chapter 1 reviews the literature relevant to the research conducted, and focuses in particular on the synthesis of β-chloroenones and related unsaturated carbonyl compounds. The synthesis of chalcone compounds from various precursors is also discussed, with particular emphasis on the use of palladium cross-coupling reactions in the preparation of these compounds. The biological activity of chalcones is also summarised in this chapter. The second chapter delineates the stereoselective synthesis of the novel α-thio-β-chloroenones from the corresponding α-thioketones in a multistep reaction cascade initiated by a NCS-mediated chlorination. A range of both alkyl and aryl β-chloroenones were prepared in this work and the oxidation of these compounds to the corresponding sulfoxides and sulfones is also outlined. The electrophilicity of the β-carbon of the enones was examined in nucleophilic addition/substitution reactions with successful access to a variety of synthetically useful novel adducts including acetals and enaminoketones. Investigation of the synthetic potential of the Stille cross-coupling reaction with the novel α-thio-β-chloroenones was explored and provided an efficient route for the synthesis of a novel series of chalcones. Most importantly this new methodology provided a new and synthetically powerful approach for carbon-carbon bond formation at the β-carbon under mild neutral conditions. A preliminary investigation into the use of these β-chloroenones as dienophiles in Diels-Alder cycloaddition reactions is also discussed in this chapter. Chapter 2 also reports the nucleophilic addition of N, O, S and C nucleophiles to previously described β-chloroacrylamides and their corresponding sulfoxide derivatives. This work builds on previous research carried out in this programme and the reactivity of these β-chloroacrylamides at the sulfide and sulfoxide level is compared. Comparison of the reactivity of the β-chloroacrylamides, in nucleophilic substitution and Stille-coupling, with that of the novel β-chloroenones is of interest. Finally, the biological activity of both the β-chloroenones and the β-chloroacrylamides in terms of cytotoxicity is summarised in Chapter 2. The final chapter, Chapter 3, details the full experimental procedures, including spectroscopic and analytical data for the compounds prepared during this research.

Catalyst, additive and substrate effects in intramolecular aromatic additions of alpha-diazoketones

This thesis is focused on transition metal catalysed reaction of α-diazoketones leading to aromatic addition to form azulenones, with particular emphasis on enantiocontrol through use of chiral copper catalysts. The first chapter provides an overview of the influence of variation of the substituent at the diazo carbon on the outcome of subsequent reaction pathways, focusing in particular on C-H insertion, cyclopropanation, aromatic addition and ylide formation drawing together for the first time input from a range of primary reports. Chapter two describes the synthesis of a range of novel α-diazoketones. Rhodium and copper catalysed cyclisation of these to form a range of azulenones is described. Variation of the transition metal catalyst was undertaken using both copper and rhodium based systems and ligand variation, including the design and synthesis of a novel bisoxazoline ligand. The influence of additives, especially NaBARF, on the enantiocontrol was explored in detail and displayed an interesting impact which was sensitive to substituent effects. Further exploration demonstrated that it is the sodium cation which is critical in the additive effects. For the first time, enantiocontrol in the aromatic addition of terminal diazoketones was demonstrated indicating enantiofacial control in the aromatic addition is feasible in the absence of a bridgehead substituent. Determination of the enantiopurity in these compounds was particularly challenging due to the lability of the products. A substantial portion of the work was focused on determining the stereochemical outcome of the aromatic addition processes, both the absolute stereochemistry and extent of enantiopurity. Formation of PTAD adducts was beneficial in this regard. The third chapter contains the full experimental details and spectral characterisation of all novel compounds synthesised in this project, while details of chiral stationary phase HPLC and 1H NMR analysis are included in the appendix.

Molecular mechanisms underpinning IFN-gamma and TNF-alpha synergy in intestinal epithelial cells

Cytokine-driven signalling shapes immune homeostasis and guides inflammatory responses mainly through induction of specific gene expression programmes both within and outside the immune cell compartment. These transcriptional outputs are often amplified via cytokine synergy, which sets a stimulatory threshold that safeguards from exacerbated inflammation and immunopathology. In this study, we investigated the molecular mechanisms underpinning synergy between two pivotal Th1 cytokines, IFN-γ and TNF-α, in human intestinal epithelial cells. These two proinflammatory mediators induce a unique state of signalling and transcriptional synergy implicated in processes such as antiviral and antitumour immunity, intestinal barrier and pancreatic β-cell dysfunction. Since its discovery more than 30 years ago, this biological phenomenon remains, however, only partially defined. Here, using a functional genomics approach including RNAi perturbation screens and small-molecule inhibitors, we identified two new regulators of IFN-γ/TNF-α-induced chemokine and antiviral gene and protein expression, a Bcl-2 protein BCL-G and a histone demethylase UTX. We also discovered that IFN-γ/TNF-α synergise to trigger a coordinated shutdown of major receptor tyrosine kinases expression in colon cancer cells. Together, these findings extend our current understanding of how IFN-γ/TNF-α synergy elicits qualitatively and quantitatively distinct outputs in the intestinal epithelium. Given the well-documented role of this synergistic state in immunopathology of various disorders, our results may help to inform the identification of high quality and biologically relevant druggable targets for diseases characterised by an IFN-γ/TNF-α high immune signature

Repeated concanavalin A challenge in mice induces an interleukin 10-producing phenotype and liver fibrosis.

Weekly injections of Concanavalin A (Con A) were performed in BALB/c mice to evaluate the pattern of cytokine production and liver injury. High serum levels of tumor necrosis factor alpha (TNF-alpha), interleukin 2 (IL-2), IL-4, and interferon gamma (IFN-gamma) were found in the serum after the first 2 injections of Con A but rapidly decreased from the third injection. Conversely, IL-10 serum levels after repeated Con A challenge increased by 7 times from week 1 to 20. In vivo depletion studies indicated that CD4(+) T cells are essential in IL-10 production. Hepatocyte necrosis was only observed after the first injections of Con A whereas centrilobular inflammatory infiltrates persisted up to 20 weeks. Perisinusoidal liver fibrosis was also increasingly detected in BALB/c mice, whereas no fibrous change was observed in nude mice after 6 weeks of Con A challenge. The number of stellate cells, detected by immunostaining, increased after 20 weeks of Con A injections. Liver cytokine messenger RNA (mRNA) expression after 20 weeks showed expression of transforming growth factor beta1 (TGF-beta1), IL-10, and IL-4 whereas IL-2 was no more expressed. The present study shows that mice repeatedly injected with Con A develop liver fibrosis. The cytokine-release pattern observed after 1 injection of Con A is rapidly shifted towards an immunomodulatory phenotype characterized by the systemic production of large amounts of IL-10.

Dose-effect of interleukin-10 and its immunoregulatory role in Crohn's disease.

BACKGROUND: Interleukin-10 (IL-10) is currently being extensively studied in clinical trials for the treatment of Crohn's disease (CD). Only marginal effects have, however, been reported, and the dose-response curve was bell-shaped contrasting with the reported data from in vitro experiments. AIM: To use another in vitro model to analyze the effect of rhIL-10 and rhIL-4 on the spontaneous mucosal TNF-alpha secretion in patients with CD, and to characterize the phenotype of the cells targeted by rhIL-10. METHODS: Non-inflamed colon biopsies from CD patients were cultured for 16 hours in presence of different concentrations of rhIL-10 or rhIL-4. The numbers of TNF-alpha-secreting cells among isolated lamina propria mononuclear cells (LPMNC) were estimated by Elispot. RESULTS: Both rhIL-10 and rhIL-4 down-regulate TNF-alpha secretion by LPMNC from CD patients, with a more pronounced effect with rhIL-10. These effects were closely linked to the cytokine concentrations used, with a bell-shaped dose-response curve. Residual TNF-alpha secretion, in the presence of optimal rhIL-10 concentration was mainly attributable to CD3+ T cells. In contrast, at higher rhIL-10 concentrations, CD3- cells contributed significantly to the TNF-alpha secretion. CONCLUSIONS: The in vitro model we used, demonstrates that IL-4, but mostly IL-10, efficiently suppresses TNF-alpha secretion in LPMNC from CD patients, with a dose-response curve similar to results obtained in vivo. Resistance at high rhIL-10 concentrations was associated with a change in the phenotype of TNF-alpha-secreting cells.

Diversion of intestinal flow decreases the numbers of interleukin 4 secreting and interferon gamma secreting T lymphocytes in small bowel mucosa.

BACKGROUND/AIMS: The intestinal immune system faces large amounts of antigens, and its regulation is tightly balanced by cytokines. In this study, the effect of intestinal flow diversion on spontaneous secretion of interleukin (IL)-4 and interferon (IFN)- gamma was analysed. METHODS: Eight patients (two with Crohn's disease, four with ulcerative colitis, and two with previous colon cancer) carrying a double lumen small bowel stoma after a total colectomy procedure were included in the study. For each patient, eight biopsy samples were taken endoscopically from both the diverted and non-diverted part of the small bowel. Intraepithelial lymphocytes (IELs) and lamina propria lymphocytes (LPLs) were isolated separately and assayed for numbers of cells spontaneously secreting IL-4 and/or IFN-gamma by an ELISPOT technique. RESULTS: Compared with the non-diverted mucosa, a significant decrease in the number of spontaneously IFN-gamma secreting CD3 lymphocytes was observed in the diverted small bowel mucosa among both IELs (p = 0.008) and LPLs (p = 0.007). The same results, although less significant, were obtained for IL-4, especially in LPLs (p = 0.01). CONCLUSION: The intestinal content influences the spontaneous secretion of IFN-gamma and IL-4 by intestinal lymphocytes. These results could help to elucidate the anti-inflammatory role of split ileostomy in patients suffering from inflammatory bowel diseases.

Helicobacter pylori modulation of gastric and duodenal mucosal T cell cytokine secretions in children compared with adults.

BACKGROUND: In contrast to adults, ulcers are un-common in Helicobacter pylori-infected children. Since immunological determinants influence the outcome of H. pylori infection, we have investigated mucosal T cell responses in H. pylori-infected children and compared them with those of adults and negative controls. MATERIAL AND METHODS: Mucosal biopsies were obtained from 43 patients undergoing an upper GI endoscopy for dyspeptic symptoms. The concentrations of released cytokines and the density of CD3+, CD25+ and CD69+cells were evaluated by flow cytometry, and the numbers of cytokine-secreting cells were measured by ELISPOT. RESULTS: The numbers of isolated antral CD3+ lymphocytes were only significantly raised in infected adults compared with noninfected controls (p < 0.05), whereas the proportion of CD3+ cells expressing activation markers (CD25 or CD69) remained low. In the stomach, IFN-gamma concentrations increased in infected children and infected adults compared with controls (p < 0.05), but IFN-gamma concentrations were tenfold lower in children than in adults (p < 0.01). IL-2, IL-4, IL-10 and TNF-alpha concentrations were similar in infected and in uninfected children and adults. In contrast, in the duodenum, IFN-gamma, as well as IL-4 and IL-10 concentrations were only increased in infected children compared with controls (p < 0.05). The concentrations of these cytokines were similar in both groups of adults who, however, like children, displayed a higher number of duodenal IL-4-secreting cells compared to controls (p < 0.05). CONCLUSION: These results suggest that IFN-gamma secretion in the stomach of H. pylori-infected patients is lower in children than in adults. This could protect children from development of severe gastro-duodenal diseases such as ulcer disease. In addition, infected patients are characterised by a dysregulation of the mucosal cytokine secretion at distance from the infection site.