@misc{15027, abstract = {This data repository underpins the paper, published in PNAS (doi pending) and bioarxiv (doi: https://doi.org/10.1101/2023.07.05.547777).}, author = {Curk, Samo}, publisher = {Figshare}, title = {{aggregation_data}}, year = {2023}, } @misc{15035, abstract = {This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties With Prefix Transducers accepted at RV'23, and give further pointers to implementation of prefix transducers. It has two parts: a pre-compiled docker image and sources that one can use to compile (locally or in docker) the software and run the experiments.}, author = {Chalupa, Marek and Henzinger, Thomas A}, publisher = {Zenodo}, title = {{Monitoring hyperproperties with prefix transducers}}, doi = {10.5281/ZENODO.8191723}, year = {2023}, } @unpublished{15039, abstract = {A crucial property for achieving secure, trustworthy and interpretable deep learning systems is their robustness: small changes to a system's inputs should not result in large changes to its outputs. Mathematically, this means one strives for networks with a small Lipschitz constant. Several recent works have focused on how to construct such Lipschitz networks, typically by imposing constraints on the weight matrices. In this work, we study an orthogonal aspect, namely the role of the activation function. We show that commonly used activation functions, such as MaxMin, as well as all piece-wise linear ones with two segments unnecessarily restrict the class of representable functions, even in the simplest one-dimensional setting. We furthermore introduce the new N-activation function that is provably more expressive than currently popular activation functions. We provide code at this https URL.}, author = {Prach, Bernd and Lampert, Christoph}, booktitle = {arXiv}, title = {{1-Lipschitz neural networks are more expressive with N-activations}}, doi = {10.48550/ARXIV.2311.06103}, year = {2023}, } @inproceedings{13053, abstract = {Deep neural networks (DNNs) often have to be compressed, via pruning and/or quantization, before they can be deployed in practical settings. In this work we propose a new compression-aware minimizer dubbed CrAM that modifies the optimization step in a principled way, in order to produce models whose local loss behavior is stable under compression operations such as pruning. Thus, dense models trained via CrAM should be compressible post-training, in a single step, without significant accuracy loss. Experimental results on standard benchmarks, such as residual networks for ImageNet classification and BERT models for language modelling, show that CrAM produces dense models that can be more accurate than the standard SGD/Adam-based baselines, but which are stable under weight pruning: specifically, we can prune models in one-shot to 70-80% sparsity with almost no accuracy loss, and to 90% with reasonable (∼1%) accuracy loss, which is competitive with gradual compression methods. Additionally, CrAM can produce sparse models which perform well for transfer learning, and it also works for semi-structured 2:4 pruning patterns supported by GPU hardware. The code for reproducing the results is available at this https URL .}, author = {Peste, Elena-Alexandra and Vladu, Adrian and Kurtic, Eldar and Lampert, Christoph and Alistarh, Dan-Adrian}, booktitle = {11th International Conference on Learning Representations }, location = {Kigali, Rwanda }, title = {{CrAM: A Compression-Aware Minimizer}}, year = {2023}, } @phdthesis{13074, abstract = {Deep learning has become an integral part of a large number of important applications, and many of the recent breakthroughs have been enabled by the ability to train very large models, capable to capture complex patterns and relationships from the data. At the same time, the massive sizes of modern deep learning models have made their deployment to smaller devices more challenging; this is particularly important, as in many applications the users rely on accurate deep learning predictions, but they only have access to devices with limited memory and compute power. One solution to this problem is to prune neural networks, by setting as many of their parameters as possible to zero, to obtain accurate sparse models with lower memory footprint. Despite the great research progress in obtaining sparse models that preserve accuracy, while satisfying memory and computational constraints, there are still many challenges associated with efficiently training sparse models, as well as understanding their generalization properties. The focus of this thesis is to investigate how the training process of sparse models can be made more efficient, and to understand the differences between sparse and dense models in terms of how well they can generalize to changes in the data distribution. We first study a method for co-training sparse and dense models, at a lower cost compared to regular training. With our method we can obtain very accurate sparse networks, and dense models that can recover the baseline accuracy. Furthermore, we are able to more easily analyze the differences, at prediction level, between the sparse-dense model pairs. Next, we investigate the generalization properties of sparse neural networks in more detail, by studying how well different sparse models trained on a larger task can adapt to smaller, more specialized tasks, in a transfer learning scenario. Our analysis across multiple pruning methods and sparsity levels reveals that sparse models provide features that can transfer similarly to or better than the dense baseline. However, the choice of the pruning method plays an important role, and can influence the results when the features are fixed (linear finetuning), or when they are allowed to adapt to the new task (full finetuning). Using sparse models with fixed masks for finetuning on new tasks has an important practical advantage, as it enables training neural networks on smaller devices. However, one drawback of current pruning methods is that the entire training cycle has to be repeated to obtain the initial sparse model, for every sparsity target; in consequence, the entire training process is costly and also multiple models need to be stored. In the last part of the thesis we propose a method that can train accurate dense models that are compressible in a single step, to multiple sparsity levels, without additional finetuning. Our method results in sparse models that can be competitive with existing pruning methods, and which can also successfully generalize to new tasks.}, author = {Peste, Elena-Alexandra}, issn = {2663-337X}, pages = {147}, publisher = {Institute of Science and Technology Austria}, title = {{Efficiency and generalization of sparse neural networks}}, doi = {10.15479/at:ista:13074}, year = {2023}, } @phdthesis{13081, abstract = {During development, tissues undergo changes in size and shape to form functional organs. Distinct cellular processes such as cell division and cell rearrangements underlie tissue morphogenesis. Yet how the distinct processes are controlled and coordinated, and how they contribute to morphogenesis is poorly understood. In our study, we addressed these questions using the developing mouse neural tube. This epithelial organ transforms from a flat epithelial sheet to an epithelial tube while increasing in size and undergoing morpho-gen-mediated patterning. The extent and mechanism of neural progenitor rearrangement within the developing mouse neuroepithelium is unknown. To investigate this, we per-formed high resolution lineage tracing analysis to quantify the extent of epithelial rear-rangement at different stages of neural tube development. We quantitatively described the relationship between apical cell size with cell cycle dependent interkinetic nuclear migra-tions (IKNM) and performed high cellular resolution live imaging of the neuroepithelium to study the dynamics of junctional remodeling. Furthermore, developed a vertex model of the neuroepithelium to investigate the quantitative contribution of cell proliferation, cell differentiation and mechanical properties to the epithelial rearrangement dynamics and validated the model predictions through functional experiments. Our analysis revealed that at early developmental stages, the apical cell area kinetics driven by IKNM induce high lev-els of cell rearrangements in a regime of high junctional tension and contractility. After E9.5, there is a sharp decline in the extent of cell rearrangements, suggesting that the epi-thelium transitions from a fluid-like to a solid-like state. We found that this transition is regulated by the growth rate of the tissue, rather than by changes in cell-cell adhesion and contractile forces. Overall, our study provides a quantitative description of the relationship between tissue growth, cell cycle dynamics, epithelia rearrangements and the emergent tissue material properties, and novel insights on how epithelial cell dynamics influences tissue morphogenesis.}, author = {Bocanegra, Laura}, issn = {2663 - 337X}, pages = {93}, publisher = {Institute of Science and Technology Austria}, title = {{Epithelial dynamics during mouse neural tube development}}, doi = {10.15479/at:ista:13081}, year = {2023}, } @article{13091, abstract = {We use a function field version of the Hardy–Littlewood circle method to study the locus of free rational curves on an arbitrary smooth projective hypersurface of sufficiently low degree. On the one hand this allows us to bound the dimension of the singular locus of the moduli space of rational curves on such hypersurfaces and, on the other hand, it sheds light on Peyre’s reformulation of the Batyrev–Manin conjecture in terms of slopes with respect to the tangent bundle.}, author = {Browning, Timothy D and Sawin, Will}, issn = {1944-7833}, journal = {Algebra and Number Theory}, number = {3}, pages = {719--748}, publisher = {Mathematical Sciences Publishers}, title = {{Free rational curves on low degree hypersurfaces and the circle method}}, doi = {10.2140/ant.2023.17.719}, volume = {17}, year = {2023}, } @article{13092, abstract = {There is a need for the development of lead-free thermoelectric materials for medium-/high-temperature applications. Here, we report a thiol-free tin telluride (SnTe) precursor that can be thermally decomposed to produce SnTe crystals with sizes ranging from tens to several hundreds of nanometers. We further engineer SnTe–Cu2SnTe3 nanocomposites with a homogeneous phase distribution by decomposing the liquid SnTe precursor containing a dispersion of Cu1.5Te colloidal nanoparticles. The presence of Cu within the SnTe and the segregated semimetallic Cu2SnTe3 phase effectively improves the electrical conductivity of SnTe while simultaneously reducing the lattice thermal conductivity without compromising the Seebeck coefficient. Overall, power factors up to 3.63 mW m–1 K–2 and thermoelectric figures of merit up to 1.04 are obtained at 823 K, which represent a 167% enhancement compared with pristine SnTe.}, author = {Nan, Bingfei and Song, Xuan and Chang, Cheng and Xiao, Ke and Zhang, Yu and Yang, Linlin and Horta, Sharona and Li, Junshan and Lim, Khak Ho and Ibáñez, Maria and Cabot, Andreu}, issn = {1944-8252}, journal = {ACS Applied Materials and Interfaces}, number = {19}, pages = {23380–23389}, publisher = {American Chemical Society}, title = {{Bottom-up synthesis of SnTe-based thermoelectric composites}}, doi = {10.1021/acsami.3c00625}, volume = {15}, year = {2023}, } @article{13093, abstract = {The direct, solid state, and reversible conversion between heat and electricity using thermoelectric devices finds numerous potential uses, especially around room temperature. However, the relatively high material processing cost limits their real applications. Silver selenide (Ag2Se) is one of the very few n-type thermoelectric (TE) materials for room-temperature applications. Herein, we report a room temperature, fast, and aqueous-phase synthesis approach to produce Ag2Se, which can be extended to other metal chalcogenides. These materials reach TE figures of merit (zT) of up to 0.76 at 380 K. To improve these values, bismuth sulfide (Bi2S3) particles also prepared in an aqueous solution are incorporated into the Ag2Se matrix. In this way, a series of Ag2Se/Bi2S3 composites with Bi2S3 wt % of 0.5, 1.0, and 1.5 are prepared by solution blending and hot-press sintering. The presence of Bi2S3 significantly improves the Seebeck coefficient and power factor while at the same time decreasing the thermal conductivity with no apparent drop in electrical conductivity. Thus, a maximum zT value of 0.96 is achieved in the composites with 1.0 wt % Bi2S3 at 370 K. Furthermore, a high average zT value (zTave) of 0.93 in the 300–390 K range is demonstrated.}, author = {Nan, Bingfei and Li, Mengyao and Zhang, Yu and Xiao, Ke and Lim, Khak Ho and Chang, Cheng and Han, Xu and Zuo, Yong and Li, Junshan and Arbiol, Jordi and Llorca, Jordi and Ibáñez, Maria and Cabot, Andreu}, issn = {2637-6113}, journal = {ACS Applied Electronic Materials}, publisher = {American Chemical Society}, title = {{Engineering of thermoelectric composites based on silver selenide in aqueous solution and ambient temperature}}, doi = {10.1021/acsaelm.3c00055}, year = {2023}, } @article{13094, abstract = {Endocytosis is a key cellular process involved in the uptake of nutrients, pathogens, or the therapy of diseases. Most studies have focused on spherical objects, whereas biologically relevant shapes can be highly anisotropic. In this letter, we use an experimental model system based on Giant Unilamellar Vesicles (GUVs) and dumbbell-shaped colloidal particles to mimic and investigate the first stage of the passive endocytic process: engulfment of an anisotropic object by the membrane. Our model has specific ligand–receptor interactions realized by mobile receptors on the vesicles and immobile ligands on the particles. Through a series of experiments, theory, and molecular dynamics simulations, we quantify the wrapping process of anisotropic dumbbells by GUVs and identify distinct stages of the wrapping pathway. We find that the strong curvature variation in the neck of the dumbbell as well as membrane tension are crucial in determining both the speed of wrapping and the final states.}, author = {Azadbakht, Ali and Meadowcroft, Billie and Varkevisser, Thijs and Šarić, Anđela and Kraft, Daniela J.}, issn = {1530-6992}, journal = {Nano Letters}, number = {10}, pages = {4267–4273}, publisher = {American Chemical Society}, title = {{Wrapping pathways of anisotropic dumbbell particles by Giant Unilamellar Vesicles}}, doi = {10.1021/acs.nanolett.3c00375}, volume = {23}, year = {2023}, } @article{13095, abstract = {Disulfide bond formation is fundamentally important for protein structure and constitutes a key mechanism by which cells regulate the intracellular oxidation state. Peroxiredoxins (PRDXs) eliminate reactive oxygen species such as hydrogen peroxide through a catalytic cycle of Cys oxidation and reduction. Additionally, upon Cys oxidation PRDXs undergo extensive conformational rearrangements that may underlie their presently structurally poorly defined functions as molecular chaperones. Rearrangements include high molecular-weight oligomerization, the dynamics of which are, however, poorly understood, as is the impact of disulfide bond formation on these properties. Here we show that formation of disulfide bonds along the catalytic cycle induces extensive μs time scale dynamics, as monitored by magic-angle spinning NMR of the 216 kDa-large Tsa1 decameric assembly and solution-NMR of a designed dimeric mutant. We ascribe the conformational dynamics to structural frustration, resulting from conflicts between the disulfide-constrained reduction of mobility and the desire to fulfill other favorable contacts.}, author = {Troussicot, Laura and Vallet, Alicia and Molin, Mikael and Burmann, Björn M. and Schanda, Paul}, issn = {1520-5126}, journal = {Journal of the American Chemical Society}, number = {19}, pages = {10700–10711}, publisher = {American Chemical Society}, title = {{Disulfide-bond-induced structural frustration and dynamic disorder in a peroxiredoxin from MAS NMR}}, doi = {10.1021/jacs.3c01200}, volume = {145}, year = {2023}, } @article{13096, abstract = {Eukaryotic cells can undergo different forms of programmed cell death, many of which culminate in plasma membrane rupture as the defining terminal event1,2,3,4,5,6,7. Plasma membrane rupture was long thought to be driven by osmotic pressure, but it has recently been shown to be in many cases an active process, mediated by the protein ninjurin-18 (NINJ1). Here we resolve the structure of NINJ1 and the mechanism by which it ruptures membranes. Super-resolution microscopy reveals that NINJ1 clusters into structurally diverse assemblies in the membranes of dying cells, in particular large, filamentous assemblies with branched morphology. A cryo-electron microscopy structure of NINJ1 filaments shows a tightly packed fence-like array of transmembrane α-helices. Filament directionality and stability is defined by two amphipathic α-helices that interlink adjacent filament subunits. The NINJ1 filament features a hydrophilic side and a hydrophobic side, and molecular dynamics simulations show that it can stably cap membrane edges. The function of the resulting supramolecular arrangement was validated by site-directed mutagenesis. Our data thus suggest that, during lytic cell death, the extracellular α-helices of NINJ1 insert into the plasma membrane to polymerize NINJ1 monomers into amphipathic filaments that rupture the plasma membrane. The membrane protein NINJ1 is therefore an interactive component of the eukaryotic cell membrane that functions as an in-built breaking point in response to activation of cell death.}, author = {Degen, Morris and Santos, José Carlos and Pluhackova, Kristyna and Cebrero, Gonzalo and Ramos, Saray and Jankevicius, Gytis and Hartenian, Ella and Guillerm, Undina and Mari, Stefania A. and Kohl, Bastian and Müller, Daniel J. and Schanda, Paul and Maier, Timm and Perez, Camilo and Sieben, Christian and Broz, Petr and Hiller, Sebastian}, issn = {1476-4687}, journal = {Nature}, pages = {1065--1071}, publisher = {Springer Nature}, title = {{Structural basis of NINJ1-mediated plasma membrane rupture in cell death}}, doi = {10.1038/s41586-023-05991-z}, volume = {618}, year = {2023}, } @article{13097, abstract = {Vertebrate movement is orchestrated by spinal inter- and motor neurons that, together with sensory and cognitive input, produce dynamic motor behaviors. These behaviors vary from the simple undulatory swimming of fish and larval aquatic species to the highly coordinated running, reaching and grasping of mice, humans and other mammals. This variation raises the fundamental question of how spinal circuits have changed in register with motor behavior. In simple, undulatory fish, exemplified by the lamprey, two broad classes of interneurons shape motor neuron output: ipsilateral-projecting excitatory neurons, and commissural-projecting inhibitory neurons. An additional class of ipsilateral inhibitory neurons is required to generate escape swim behavior in larval zebrafish and tadpoles. In limbed vertebrates, a more complex spinal neuron composition is observed. In this review, we provide evidence that movement elaboration correlates with an increase and specialization of these three basic interneuron types into molecularly, anatomically, and functionally distinct subpopulations. We summarize recent work linking neuron types to movement-pattern generation across fish, amphibians, reptiles, birds and mammals.}, author = {Wilson, Alexia C and Sweeney, Lora Beatrice Jaeger}, issn = {1662-5110}, journal = {Frontiers in Neural Circuits}, publisher = {Frontiers}, title = {{Spinal cords: Symphonies of interneurons across species}}, doi = {10.3389/fncir.2023.1146449}, volume = {17}, year = {2023}, } @phdthesis{13106, abstract = {Quantum entanglement is a key resource in currently developed quantum technologies. Sharing this fragile property between superconducting microwave circuits and optical or atomic systems would enable new functionalities, but this has been hindered by an energy scale mismatch of >104 and the resulting mutually imposed loss and noise. In this work, we created and verified entanglement between microwave and optical fields in a millikelvin environment. Using an optically pulsed superconducting electro-optical device, we show entanglement between propagating microwave and optical fields in the continuous variable domain. This achievement not only paves the way for entanglement between superconducting circuits and telecom wavelength light, but also has wide-ranging implications for hybrid quantum networks in the context of modularization, scaling, sensing, and cross-platform verification.}, author = {Sahu, Rishabh and Qiu, Liu and Hease, William J and Arnold, Georg M and Minoguchi, Y. and Rabl, P. and Fink, Johannes M}, issn = {1095-9203}, keywords = {Multidisciplinary}, pages = {718--721}, publisher = {American Association for the Advancement of Science}, title = {{Entangling microwaves with light}}, doi = {10.1126/science.adg3812}, volume = {380}, year = {2023}, } @phdthesis{13107, abstract = {Within the human body, the brain exhibits the highest rate of energy consumption amongst all organs, with the majority of generated ATP being utilized to sustain neuronal activity. Therefore, the metabolism of the mature cerebral cortex is geared towards preserving metabolic homeostasis whilst generating significant amounts of energy. This requires a precise interplay between diverse metabolic pathways, spanning from a tissue-wide scale to the level of individual neurons. Disturbances to this delicate metabolic equilibrium, such as those resulting from maternal malnutrition or mutations affecting metabolic enzymes, often result in neuropathological variants of neurodevelopment. For instance, mutations in SLC7A5, a transporter of metabolically essential large neutral amino acids (LNAAs), have been associated with autism and microcephaly. However, despite recent progress in the field, the extent of metabolic restructuring that occurs within the developing brain and the corresponding alterations in nutrient demands during various critical periods remain largely unknown. To investigate this, we performed metabolomic profiling of the murine cerebral cortex to characterize the metabolic state of the forebrain at different developmental stages. We found that the developing cortex undergoes substantial metabolic reprogramming, with specific sets of metabolites displaying stage-specific changes. According to our observations, we determined a distinct temporal period in postnatal development during which the cortex displays heightened reliance on LNAAs. Hence, using a conditional knock-out mouse model, we deleted Slc7a5 in neural cells, allowing us to monitor the impact of a perturbed neuronal metabolic state across multiple developmental stages of corticogenesis. We found that manipulating the levels of essential LNAAs in cortical neurons in vivo affects one particular perinatal developmental period critical for cortical network refinement. Abnormally low intracellular LNAA levels result in cell-autonomous alterations in neuronal lipid metabolism, excitability, and survival during this particular time window. Although most of the effects of Slc7a5 deletion on neuronal physiology are transient, derailment of these processes during this brief but crucial window leads to long-term circuit dysfunction in mice. In conclusion, out data indicate that the cerebral cortex undergoes significant metabolic reorganization during development. This process involves the intricate integration of multiple metabolic pathways to ensure optimal neuronal function throughout different developmental stages. Our findings offer a paradigm for understanding how neurons synchronize the expression of nutrient-related genes with their activity to allow proper brain maturation. Further, our results demonstrate that disruptions in these precisely calibrated metabolic processes during critical periods of brain development may result in neuropathological outcomes in mice and in humans.}, author = {Knaus, Lisa}, issn = {2663 - 337X}, pages = {147}, publisher = {Institute of Science and Technology Austria}, title = {{The metabolism of the developing brain : How large neutral amino acids modulate perinatal neuronal excitability and survival}}, doi = {10.15479/at:ista:13107}, year = {2023}, } @misc{13116, abstract = {The emergence of large-scale order in self-organized systems relies on local interactions between individual components. During bacterial cell division, FtsZ -- a prokaryotic homologue of the eukaryotic protein tubulin -- polymerizes into treadmilling filaments that further organize into a cytoskeletal ring. In vitro, FtsZ filaments can form dynamic chiral assemblies. However, how the active and passive properties of individual filaments relate to these large-scale self-organized structures remains poorly understood. Here, we connect single filament properties with the mesoscopic scale by combining minimal active matter simulations and biochemical reconstitution experiments. We show that density and flexibility of active chiral filaments define their global order. At intermediate densities, curved, flexible filaments organize into chiral rings and polar bands. An effectively nematic organization dominates for high densities and for straight, mutant filaments with increased rigidity. Our predicted phase diagram captures these features quantitatively, demonstrating how the flexibility, density and chirality of active filaments affect their collective behaviour. Our findings shed light on the fundamental properties of active chiral matter and explain how treadmilling FtsZ filaments organize during bacterial cell division. }, author = {Dunajova, Zuzana and Prats Mateu, Batirtze and Radler, Philipp and Lim, Keesiang and Brandis, Dörte and Velicky, Philipp and Danzl, Johann G and Wong, Richard W. and Elgeti, Jens and Hannezo, Edouard B and Loose, Martin}, publisher = {Institute of Science and Technology Austria}, title = {{Chiral and nematic phases of flexible active filaments}}, doi = {10.15479/AT:ISTA:13116}, year = {2023}, } @article{13117, abstract = {The ability to control the direction of scattered light is crucial to provide flexibility and scalability for a wide range of on-chip applications, such as integrated photonics, quantum information processing, and nonlinear optics. Tunable directionality can be achieved by applying external magnetic fields that modify optical selection rules, by using nonlinear effects, or interactions with vibrations. However, these approaches are less suitable to control microwave photon propagation inside integrated superconducting quantum devices. Here, we demonstrate on-demand tunable directional scattering based on two periodically modulated transmon qubits coupled to a transmission line at a fixed distance. By changing the relative phase between the modulation tones, we realize unidirectional forward or backward photon scattering. Such an in-situ switchable mirror represents a versatile tool for intra- and inter-chip microwave photonic processors. In the future, a lattice of qubits can be used to realize topological circuits that exhibit strong nonreciprocity or chirality.}, author = {Redchenko, Elena and Poshakinskiy, Alexander V. and Sett, Riya and Zemlicka, Martin and Poddubny, Alexander N. and Fink, Johannes M}, issn = {2041-1723}, journal = {Nature Communications}, publisher = {Springer Nature}, title = {{Tunable directional photon scattering from a pair of superconducting qubits}}, doi = {10.1038/s41467-023-38761-6}, volume = {14}, year = {2023}, } @article{13118, abstract = {Under high pressures and temperatures, molecular systems with substantial polarization charges, such as ammonia and water, are predicted to form superionic phases and dense fluid states with dissociating molecules and high electrical conductivity. This behaviour potentially plays a role in explaining the origin of the multipolar magnetic fields of Uranus and Neptune, whose mantles are thought to result from a mixture of H2O, NH3 and CH4 ices. Determining the stability domain, melting curve and electrical conductivity of these superionic phases is therefore crucial for modelling planetary interiors and dynamos. Here we report the melting curve of superionic ammonia up to 300 GPa from laser-driven shock compression of pre-compressed samples and atomistic calculations. We show that ammonia melts at lower temperatures than water above 100 GPa and that fluid ammonia’s electrical conductivity exceeds that of water at conditions predicted by hot, super-adiabatic models for Uranus and Neptune, and enhances the conductivity in their fluid water-rich dynamo layers.}, author = {Hernandez, J.-A. and Bethkenhagen, Mandy and Ninet, S. and French, M. and Benuzzi-Mounaix, A. and Datchi, F. and Guarguaglini, M. and Lefevre, F. and Occelli, F. and Redmer, R. and Vinci, T. and Ravasio, A.}, issn = {1745-2481}, journal = {Nature Physics}, pages = {1280--1285}, publisher = {Springer Nature}, title = {{Melting curve of superionic ammonia at planetary interior conditions}}, doi = {10.1038/s41567-023-02074-8}, volume = {19}, year = {2023}, } @article{13119, abstract = {A density wave (DW) is a fundamental type of long-range order in quantum matter tied to self-organization into a crystalline structure. The interplay of DW order with superfluidity can lead to complex scenarios that pose a great challenge to theoretical analysis. In the past decades, tunable quantum Fermi gases have served as model systems for exploring the physics of strongly interacting fermions, including most notably magnetic ordering1, pairing and superfluidity2, and the crossover from a Bardeen–Cooper–Schrieffer superfluid to a Bose–Einstein condensate3. Here, we realize a Fermi gas featuring both strong, tunable contact interactions and photon-mediated, spatially structured long-range interactions in a transversely driven high-finesse optical cavity. Above a critical long-range interaction strength, DW order is stabilized in the system, which we identify via its superradiant light-scattering properties. We quantitatively measure the variation of the onset of DW order as the contact interaction is varied across the Bardeen–Cooper–Schrieffer superfluid and Bose–Einstein condensate crossover, in qualitative agreement with a mean-field theory. The atomic DW susceptibility varies over an order of magnitude upon tuning the strength and the sign of the long-range interactions below the self-ordering threshold, demonstrating independent and simultaneous control over the contact and long-range interactions. Therefore, our experimental setup provides a fully tunable and microscopically controllable platform for the experimental study of the interplay of superfluidity and DW order.}, author = {Helson, Victor and Zwettler, Timo and Mivehvar, Farokh and Colella, Elvia and Roux, Kevin Etienne Robert and Konishi, Hideki and Ritsch, Helmut and Brantut, Jean Philippe}, issn = {1476-4687}, journal = {Nature}, pages = {716--720}, publisher = {Springer Nature}, title = {{Density-wave ordering in a unitary Fermi gas with photon-mediated interactions}}, doi = {10.1038/s41586-023-06018-3}, volume = {618}, year = {2023}, } @inproceedings{13120, abstract = {We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction.}, author = {Dvorak, Martin and Blanchette, Jasmin}, booktitle = {14th International Conference on Interactive Theorem Proving}, isbn = {9783959772846}, issn = {1868-8969}, location = {Bialystok, Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Closure properties of general grammars - formally verified}}, doi = {10.4230/LIPIcs.ITP.2023.15}, volume = {268}, year = {2023}, }