Lymphopenia is associated with broad host response aberrations in community-acquired pneumonia.

OBJECTIVES: Lymphopenia at hospital admission occurs in over one-third of patients with community-acquired pneumonia (CAP), yet its clinical relevance and pathophysiological implications remain underexplored. We evaluated outcomes and immune features of patients with lymphopenic CAP (L-CAP), a previously described immunophenotype characterized by admission lymphocyte count <0.724 × 109 cells/L. METHODS: Observational study in 149 patients admitted to a general ward for CAP. We measured 34 plasma biomarkers reflective of inflammation, endothelial cell responses, coagulation, and immune checkpoints. We characterized lymphocyte phenotypes in 29 patients using spectral flow cytometry. RESULTS: L-CAP occurred in 45 patients (30.2%) and was associated with prolonged time-to-clinical-stability (median 5 versus 3 days), also when we accounted for competing events for reaching clinical stability and adjusted for baseline covariates (subdistribution hazard ratio 0.63; 95% confidence interval 0.45-0.88). L-CAP patients demonstrated a proportional depletion of CD4 T follicular helper cells, CD4 T effector memory cells, naïve CD8 T cells and IgG+ B cells. Plasma biomarker analyses indicated increased activation of the cytokine network and the vascular endothelium in L-CAP. CONCLUSIONS: L-CAP patients have a protracted clinical recovery course and a more broadly dysregulated host response. These findings highlight the prognostic and pathophysiological relevance of admission lymphopenia in patients with CAP.

The shifting lipidomic landscape of blood monocytes and neutrophils during pneumonia.

The lipidome of immune cells during infection has remained unexplored, although evidence of the importance of lipids in the context of immunity is mounting. In this study, we performed untargeted lipidomic analysis of blood monocytes and neutrophils from patients hospitalized for pneumonia and age- and sex-matched noninfectious control volunteers. We annotated 521 and 706 lipids in monocytes and neutrophils, respectively, which were normalized to an extensive set of internal standards per lipid class. The cellular lipidomes were profoundly altered in patients, with both common and distinct changes between the cell types. Changes involved every level of the cellular lipidome: differential lipid species, class-wide shifts, and altered saturation patterns. Overall, differential lipids were mainly less abundant in monocytes and more abundant in neutrophils from patients. One month after hospital admission, lipidomic changes were fully resolved in monocytes and partially in neutrophils. Integration of lipidomic and concurrently collected transcriptomic data highlighted altered sphingolipid metabolism in both cell types. Inhibition of ceramide and sphingosine-1-phosphate synthesis in healthy monocytes and neutrophils resulted in blunted cytokine responses upon stimulation with lipopolysaccharide. These data reveal major lipidomic remodeling in immune cells during infection, and link the cellular lipidome to immune functionality.

Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL.

The LLL basis reduction algorithm was the first polynomial-time algorithm to compute a reduced basis of a given lattice, and hence also a short vector in the lattice. It approximates an NP-hard problem where the approximation quality solely depends on the dimension of the lattice, but not the lattice itself. The algorithm has applications in number theory, computer algebra and cryptography. In this paper, we provide an implementation of the LLL algorithm. Both its soundness and its polynomial running-time have been verified using Isabelle/HOL. Our implementation is nearly as fast as an implementation in a commercial computer algebra system, and its efficiency can be further increased by connecting it with fast untrusted lattice reduction algorithms and certifying their output. We additionally integrate one application of LLL, namely a verified factorization algorithm for univariate integer polynomials which runs in polynomial time.

A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm.

We formally verify the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs factorization in the prime field GF ( p ) and then performs computations in the ring of integers modulo p k , where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.

A Verified Implementation of Algebraic Numbers in Isabelle/HOL.

We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle's code generator. The development combines various existing formalizations such as matrices, Sturm's theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.