@inproceedings{8194, abstract = {Fixed-point arithmetic is a popular alternative to floating-point arithmetic on embedded systems. Existing work on the verification of fixed-point programs relies on custom formalizations of fixed-point arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of fixed-point arithmetic. We present an intuitive yet comprehensive syntax of the fixed-point theory, and provide formal semantics for it based on rational arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.}, author = {Baranowski, Marek and He, Shaobo and Lechner, Mathias and Nguyen, Thanh Son and Rakamarić, Zvonimir}, booktitle = {Automated Reasoning}, isbn = {9783030510732}, issn = {16113349}, location = {Paris, France}, pages = {13--31}, publisher = {Springer Nature}, title = {{An SMT theory of fixed-point arithmetic}}, doi = {10.1007/978-3-030-51074-9_2}, volume = {12166}, year = {2020}, } @article{8220, abstract = {Understanding to what extent stem cell potential is a cell-intrinsic property or an emergent behavior coming from global tissue dynamics and geometry is a key outstanding question of systems and stem cell biology. Here, we propose a theory of stem cell dynamics as a stochastic competition for access to a spatially localized niche, giving rise to a stochastic conveyor-belt model. Cell divisions produce a steady cellular stream which advects cells away from the niche, while random rearrangements enable cells away from the niche to be favorably repositioned. Importantly, even when assuming that all cells in a tissue are molecularly equivalent, we predict a common (“universal”) functional dependence of the long-term clonal survival probability on distance from the niche, as well as the emergence of a well-defined number of functional stem cells, dependent only on the rate of random movements vs. mitosis-driven advection. We test the predictions of this theory on datasets of pubertal mammary gland tips and embryonic kidney tips, as well as homeostatic intestinal crypts. Importantly, we find good agreement for the predicted functional dependency of the competition as a function of position, and thus functional stem cell number in each organ. This argues for a key role of positional fluctuations in dictating stem cell number and dynamics, and we discuss the applicability of this theory to other settings.}, author = {Corominas-Murtra, Bernat and Scheele, Colinda L.G.J. and Kishi, Kasumi and Ellenbroek, Saskia I.J. and Simons, Benjamin D. and Van Rheenen, Jacco and Hannezo, Edouard B}, issn = {10916490}, journal = {Proceedings of the National Academy of Sciences of the United States of America}, number = {29}, pages = {16969--16975}, publisher = {National Academy of Sciences}, title = {{Stem cell lineage survival as a noisy competition for niche access}}, doi = {10.1073/pnas.1921205117}, volume = {117}, year = {2020}, } @article{8199, abstract = {We investigate a mechanism to transiently stabilize topological phenomena in long-lived quasi-steady states of isolated quantum many-body systems driven at low frequencies. We obtain an analytical bound for the lifetime of the quasi-steady states which is exponentially large in the inverse driving frequency. Within this lifetime, the quasi-steady state is characterized by maximum entropy subject to the constraint of fixed number of particles in the system's Floquet-Bloch bands. In such a state, all the non-universal properties of these bands are washed out, hence only the topological properties persist.}, author = {Gulden, Tobias and Berg, Erez and Rudner, Mark Spencer and Lindner, Netanel}, issn = {2542-4653}, journal = {SciPost Physics}, publisher = {SciPost Foundation}, title = {{Exponentially long lifetime of universal quasi-steady states in topological Floquet pumps}}, doi = {10.21468/scipostphys.9.1.015}, volume = {9}, year = {2020}, } @article{8261, abstract = {Dentate gyrus granule cells (GCs) connect the entorhinal cortex to the hippocampal CA3 region, but how they process spatial information remains enigmatic. To examine the role of GCs in spatial coding, we measured excitatory postsynaptic potentials (EPSPs) and action potentials (APs) in head-fixed mice running on a linear belt. Intracellular recording from morphologically identified GCs revealed that most cells were active, but activity level varied over a wide range. Whereas only ∼5% of GCs showed spatially tuned spiking, ∼50% received spatially tuned input. Thus, the GC population broadly encodes spatial information, but only a subset relays this information to the CA3 network. Fourier analysis indicated that GCs received conjunctive place-grid-like synaptic input, suggesting code conversion in single neurons. GC firing was correlated with dendritic complexity and intrinsic excitability, but not extrinsic excitatory input or dendritic cable properties. Thus, functional maturation may control input-output transformation and spatial code conversion.}, author = {Zhang, Xiaomin and Schlögl, Alois and Jonas, Peter M}, issn = {0896-6273}, journal = {Neuron}, number = {6}, pages = {1212--1225}, publisher = {Elsevier}, title = {{Selective routing of spatial information flow from input to output in hippocampal granule cells}}, doi = {10.1016/j.neuron.2020.07.006}, volume = {107}, year = {2020}, } @article{8268, abstract = {Modern scientific instruments produce vast amounts of data, which can overwhelm the processing ability of computer systems. Lossy compression of data is an intriguing solution, but comes with its own drawbacks, such as potential signal loss, and the need for careful optimization of the compression ratio. In this work, we focus on a setting where this problem is especially acute: compressive sensing frameworks for interferometry and medical imaging. We ask the following question: can the precision of the data representation be lowered for all inputs, with recovery guarantees and practical performance Our first contribution is a theoretical analysis of the normalized Iterative Hard Thresholding (IHT) algorithm when all input data, meaning both the measurement matrix and the observation vector are quantized aggressively. We present a variant of low precision normalized IHT that, under mild conditions, can still provide recovery guarantees. The second contribution is the application of our quantization framework to radio astronomy and magnetic resonance imaging. We show that lowering the precision of the data can significantly accelerate image recovery. We evaluate our approach on telescope data and samples of brain images using CPU and FPGA implementations achieving up to a 9x speedup with negligible loss of recovery quality.}, author = {Gurel, Nezihe Merve and Kara, Kaan and Stojanov, Alen and Smith, Tyler and Lemmin, Thomas and Alistarh, Dan-Adrian and Puschel, Markus and Zhang, Ce}, issn = {19410476}, journal = {IEEE Transactions on Signal Processing}, pages = {4268--4282}, publisher = {IEEE}, title = {{Compressive sensing using iterative hard thresholding with low precision data representation: Theory and applications}}, doi = {10.1109/TSP.2020.3010355}, volume = {68}, year = {2020}, } @article{8101, abstract = {By rigorously accounting for mesoscale spatial correlations in donor/acceptor surface properties, we develop a scale-spanning model for same-material tribocharging. We find that mesoscale correlations affect not only the magnitude of charge transfer but also the fluctuations—suppressing otherwise overwhelming charge-transfer variability that is not observed experimentally. We furthermore propose a generic theoretical mechanism by which the mesoscale features might emerge, which is qualitatively consistent with other proposals in the literature.}, author = {Grosjean, Galien M and Wald, Sebastian and Sobarzo Ponce, Juan Carlos A and Waitukaitis, Scott R}, issn = {2475-9953}, journal = {Physical Review Materials}, keywords = {electric charge, tribocharging, soft matter, granular materials, polymers}, number = {8}, publisher = {American Physical Society}, title = {{Quantitatively consistent scale-spanning model for same-material tribocharging}}, doi = {10.1103/PhysRevMaterials.4.082602}, volume = {4}, year = {2020}, } @article{8325, abstract = {Let 𝐹:ℤ2→ℤ be the pointwise minimum of several linear functions. The theory of smoothing allows us to prove that under certain conditions there exists the pointwise minimal function among all integer-valued superharmonic functions coinciding with F “at infinity”. We develop such a theory to prove existence of so-called solitons (or strings) in a sandpile model, studied by S. Caracciolo, G. Paoletti, and A. Sportiello. Thus we made a step towards understanding the phenomena of the identity in the sandpile group for planar domains where solitons appear according to experiments. We prove that sandpile states, defined using our smoothing procedure, move changeless when we apply the wave operator (that is why we call them solitons), and can interact, forming triads and nodes. }, author = {Kalinin, Nikita and Shkolnikov, Mikhail}, issn = {14320916}, journal = {Communications in Mathematical Physics}, number = {9}, pages = {1649--1675}, publisher = {Springer Nature}, title = {{Sandpile solitons via smoothing of superharmonic functions}}, doi = {10.1007/s00220-020-03828-8}, volume = {378}, year = {2020}, } @article{8318, abstract = {Complex I is the first and the largest enzyme of respiratory chains in bacteria and mitochondria. The mechanism which couples spatially separated transfer of electrons to proton translocation in complex I is not known. Here we report five crystal structures of T. thermophilus enzyme in complex with NADH or quinone-like compounds. We also determined cryo-EM structures of major and minor native states of the complex, differing in the position of the peripheral arm. Crystal structures show that binding of quinone-like compounds (but not of NADH) leads to a related global conformational change, accompanied by local re-arrangements propagating from the quinone site to the nearest proton channel. Normal mode and molecular dynamics analyses indicate that these are likely to represent the first steps in the proton translocation mechanism. Our results suggest that quinone binding and chemistry play a key role in the coupling mechanism of complex I.}, author = {Gutierrez-Fernandez, Javier and Kaszuba, Karol and Minhas, Gurdeep S. and Baradaran, Rozbeh and Tambalo, Margherita and Gallagher, David T. and Sazanov, Leonid A}, issn = {20411723}, journal = {Nature Communications}, number = {1}, publisher = {Springer Nature}, title = {{Key role of quinone in the mechanism of respiratory complex I}}, doi = {10.1038/s41467-020-17957-0}, volume = {11}, year = {2020}, } @article{8323, author = {Pach, János}, issn = {14320444}, journal = {Discrete and Computational Geometry}, pages = {571--574}, publisher = {Springer Nature}, title = {{A farewell to Ricky Pollack}}, doi = {10.1007/s00454-020-00237-5}, volume = {64}, year = {2020}, } @article{8336, abstract = {Plant hormone cytokinins are perceived by a subfamily of sensor histidine kinases (HKs), which via a two-component phosphorelay cascade activate transcriptional responses in the nucleus. Subcellular localization of the receptors proposed the endoplasmic reticulum (ER) membrane as a principal cytokinin perception site, while study of cytokinin transport pointed to the plasma membrane (PM)-mediated cytokinin signalling. Here, by detailed monitoring of subcellular localizations of the fluorescently labelled natural cytokinin probe and the receptor ARABIDOPSIS HISTIDINE KINASE 4 (CRE1/AHK4) fused to GFP reporter, we show that pools of the ER-located cytokinin receptors can enter the secretory pathway and reach the PM in cells of the root apical meristem, and the cell plate of dividing meristematic cells. Brefeldin A (BFA) experiments revealed vesicular recycling of the receptor and its accumulation in BFA compartments. We provide a revised view on cytokinin signalling and the possibility of multiple sites of perception at PM and ER.}, author = {Kubiasova, Karolina and Montesinos López, Juan C and Šamajová, Olga and Nisler, Jaroslav and Mik, Václav and Semeradova, Hana and Plíhalová, Lucie and Novák, Ondřej and Marhavý, Peter and Cavallari, Nicola and Zalabák, David and Berka, Karel and Doležal, Karel and Galuszka, Petr and Šamaj, Jozef and Strnad, Miroslav and Benková, Eva and Plíhal, Ondřej and Spíchal, Lukáš}, issn = {20411723}, journal = {Nature Communications}, publisher = {Springer Nature}, title = {{Cytokinin fluoroprobe reveals multiple sites of cytokinin perception at plasma membrane and endoplasmic reticulum}}, doi = {10.1038/s41467-020-17949-0}, volume = {11}, year = {2020}, }