@article{10173, abstract = {We study the large scale behavior of elliptic systems with stationary random coefficient that have only slowly decaying correlations. To this aim we analyze the so-called corrector equation, a degenerate elliptic equation posed in the probability space. In this contribution, we use a parabolic approach and optimally quantify the time decay of the semigroup. For the theoretical point of view, we prove an optimal decay estimate of the gradient and flux of the corrector when spatially averaged over a scale R larger than 1. For the numerical point of view, our results provide convenient tools for the analysis of various numerical methods.}, author = {Clozeau, Nicolas}, issn = {2194-0401}, journal = {Stochastics and Partial Differential Equations: Analysis and Computations}, pages = {1254–1378}, publisher = {Springer Nature}, title = {{Optimal decay of the parabolic semigroup in stochastic homogenization for correlated coefficient fields}}, doi = {10.1007/s40072-022-00254-w}, volume = {11}, year = {2023}, } @article{10174, abstract = {Quantitative stochastic homogenization of linear elliptic operators is by now well-understood. In this contribution we move forward to the nonlinear setting of monotone operators with p-growth. This first work is dedicated to a quantitative two-scale expansion result. Fluctuations will be addressed in companion articles. By treating the range of exponents 2≤p<∞ in dimensions d≤3, we are able to consider genuinely nonlinear elliptic equations and systems such as −∇⋅A(x)(1+|∇u|p−2)∇u=f (with A random, non-necessarily symmetric) for the first time. When going from p=2 to p>2, the main difficulty is to analyze the associated linearized operator, whose coefficients are degenerate, unbounded, and depend on the random input A via the solution of a nonlinear equation. One of our main achievements is the control of this intricate nonlinear dependence, leading to annealed Meyers' estimates for the linearized operator, which are key to the quantitative two-scale expansion result.}, author = {Clozeau, Nicolas and Gloria, Antoine}, issn = {1432-0673}, journal = {Archive for Rational Mechanics and Analysis }, number = {4}, publisher = {Springer Nature}, title = {{Quantitative nonlinear homogenization: Control of oscillations}}, doi = {10.1007/s00205-023-01895-4}, volume = {247}, year = {2023}, } @article{10405, abstract = {We consider large non-Hermitian random matrices X with complex, independent, identically distributed centred entries and show that the linear statistics of their eigenvalues are asymptotically Gaussian for test functions having 2+ϵ derivatives. Previously this result was known only for a few special cases; either the test functions were required to be analytic [72], or the distribution of the matrix elements needed to be Gaussian [73], or at least match the Gaussian up to the first four moments [82, 56]. We find the exact dependence of the limiting variance on the fourth cumulant that was not known before. The proof relies on two novel ingredients: (i) a local law for a product of two resolvents of the Hermitisation of X with different spectral parameters and (ii) a coupling of several weakly dependent Dyson Brownian motions. These methods are also the key inputs for our analogous results on the linear eigenvalue statistics of real matrices X that are presented in the companion paper [32]. }, author = {Cipolloni, Giorgio and Erdös, László and Schröder, Dominik J}, issn = {1097-0312}, journal = {Communications on Pure and Applied Mathematics}, number = {5}, pages = {946--1034}, publisher = {Wiley}, title = {{Central limit theorem for linear eigenvalue statistics of non-Hermitian random matrices}}, doi = {10.1002/cpa.22028}, volume = {76}, year = {2023}, } @article{10550, abstract = {The global existence of renormalised solutions and convergence to equilibrium for reaction-diffusion systems with non-linear diffusion are investigated. The system is assumed to have quasi-positive non-linearities and to satisfy an entropy inequality. The difficulties in establishing global renormalised solutions caused by possibly degenerate diffusion are overcome by introducing a new class of weighted truncation functions. By means of the obtained global renormalised solutions, we study the large-time behaviour of complex balanced systems arising from chemical reaction network theory with non-linear diffusion. When the reaction network does not admit boundary equilibria, the complex balanced equilibrium is shown, by using the entropy method, to exponentially attract all renormalised solutions in the same compatibility class. This convergence extends even to a range of non-linear diffusion, where global existence is an open problem, yet we are able to show that solutions to approximate systems converge exponentially to equilibrium uniformly in the regularisation parameter.}, author = {Fellner, Klemens and Fischer, Julian L and Kniely, Michael and Tang, Bao Quoc}, issn = {1432-1467}, journal = {Journal of Nonlinear Science}, publisher = {Springer Nature}, title = {{Global renormalised solutions and equilibration of reaction-diffusion systems with non-linear diffusion}}, doi = {10.1007/s00332-023-09926-w}, volume = {33}, year = {2023}, } @article{10551, abstract = {The Dean–Kawasaki equation—a strongly singular SPDE—is a basic equation of fluctuating hydrodynamics; it has been proposed in the physics literature to describe the fluctuations of the density of N independent diffusing particles in the regime of large particle numbers N≫1. The singular nature of the Dean–Kawasaki equation presents a substantial challenge for both its analysis and its rigorous mathematical justification. Besides being non-renormalisable by the theory of regularity structures by Hairer et al., it has recently been shown to not even admit nontrivial martingale solutions. In the present work, we give a rigorous and fully quantitative justification of the Dean–Kawasaki equation by considering the natural regularisation provided by standard numerical discretisations: We show that structure-preserving discretisations of the Dean–Kawasaki equation may approximate the density fluctuations of N non-interacting diffusing particles to arbitrary order in N−1 (in suitable weak metrics). In other words, the Dean–Kawasaki equation may be interpreted as a “recipe” for accurate and efficient numerical simulations of the density fluctuations of independent diffusing particles.}, author = {Cornalba, Federico and Fischer, Julian L}, issn = {1432-0673}, journal = {Archive for Rational Mechanics and Analysis}, number = {5}, publisher = {Springer Nature}, title = {{The Dean-Kawasaki equation and the structure of density fluctuations in systems of diffusing particles}}, doi = {10.1007/s00205-023-01903-7}, volume = {247}, year = {2023}, } @article{20966, abstract = {We prepared a series of water‐soluble aromatic oligoamide sequences all composed of a segment prone to form a single helix and a segment prone to dimerize into a double helix. These sequences exclusively assemble as antiparallel duplexes. The modification of the duplex inner rim by varying the nature of the substituents borne by the aromatic monomers allowed us to identify sequences that can hybridize by combining two chemically different strands, with high affinity and complete selectivity in water. X‐ray crystallography confirmed the expected antiparallel configuration of the duplexes whereas NMR spectroscopy and mass spectrometry allowed us to assess precisely the extent of the hybridization. The hybridization kinetics of the aromatic strands was shown to depend on both the nature of the substituents responsible for strand complementarity and the length of the aromatic strand. These results highlight the great potential of aromatic hetero‐duplex as a tool to construct non‐symmetrical dynamic supramolecular assemblies.}, author = {Koehler, Victor and Bruschera, Gabrielle and Merlet, Eric and Mandal, Pradeep K and Morvan, Estelle and Rosu, Frédéric and Douat, Céline and Fischer, Lucile and Huc, Ivan and Ferrand, Yann}, issn = {1521-3773}, journal = {Angewandte Chemie International Edition}, number = {48}, publisher = {Wiley}, title = {{High‐affinity hybridization of complementary aromatic oligoamide strands in water}}, doi = {10.1002/anie.202311639}, volume = {62}, year = {2023}, } @article{20968, abstract = {Several helically folded aromatic oligoamides were designed and synthesized. The sequences were all water-soluble thanks to the charged side chains borne by the monomers. Replacing a few, sometimes only two, charged side chains by neutral methoxy groups was shown to trigger the formation of various aggregates which could be tentatively assigned to head-to-head stacked dimers of single helices, double helical duplexes and a quadruplex, none of which would form in organic solvent with organic-soluble analogues. The nature of the aggregates was supported by concentration and solvent dependent NMR studies, 1H DOSY experiments, mass spectrometry, and X-ray crystallography or energy-minimized models, as well as analogies with earlier studies. The hydrophobic effect appears to be the main driving force for aggregation but it can be finely modulated by the presence or absence of a small number of charges to an extent that had no precedent in aromatic foldamer architectures. These results will serve as a benchmark for future foldamer design in water.}, author = {Teng, Binhao and Mandal, Pradeep K and Allmendinger, Lars and Douat, Céline and Ferrand, Yann and Huc, Ivan}, issn = {2041-6539}, journal = {Chemical Science}, number = {40}, pages = {11251--11260}, publisher = {Royal Society of Chemistry}, title = {{Controlling aromatic helix dimerization in water by tuning charge repulsions}}, doi = {10.1039/d3sc02020g}, volume = {14}, year = {2023}, } @article{20969, abstract = {The diastereoselective assembly of achiral constituents through a single spontaneous process into complex covalent architectures bearing multiple stereogenic elements still remains a challenge for synthetic chemists. Here, we show that such an extreme level of control can be achieved by implementing stereo-electronic information on synthetic organic building blocks and templates and that non-directional interactions (i.e., electrostatic and steric interactions) can transfer this information to deliver, after self-assembly, high-molecular weight macrocyclic species carrying up to 16 stereogenic elements. Beyond the field of supramolecular chemistry, this proof of concept should stimulate the on-demand production of highly structured polyfunctional architectures.}, author = {Zhang, Yuan and Ourri, Benjamin and Skowron, Pierre-Thomas and Jeamet, Emeric and Chetot, Titouan and Duchamp, Christian and Belenguer, Ana M. and Vanthuyne, Nicolas and Cala, Olivier and Dumont, Elise and Mandal, Pradeep K and Huc, Ivan and Perret, Florent and Vial, Laurent and Leclaire, Julien}, issn = {2041-6539}, journal = {Chemical Science}, number = {26}, pages = {7126--7135}, publisher = {Royal Society of Chemistry}, title = {{Self-assembly of achiral building blocks into chiral cyclophanes using non-directional interactions}}, doi = {10.1039/d3sc01235b}, volume = {14}, year = {2023}, } @article{20970, abstract = {Dynamic foldamers are synthetic folded molecules which can change their conformation in response to an external stimulus and are currently at the forefront of foldamer chemistry. However, constitutionally dynamic foldamers, which can change not only their conformation but also their molecular constitution in response to their environment, are without precedent. We now report a size- and shape-switching small dynamic covalent foldamer network which responds to changes in pH. Specifically, acidic conditions direct the oligomerization of a dipeptide-based building block into a 16-subunit macrocycle with well-defined conformation and with high selectivity. At higher pH the same building block yields another cyclic foldamer with a smaller ring size (9mer). The two foldamers readily and repeatedly interconvert upon adjustment of the pH of the solution. We have previously shown that addition of a template can direct oligomerization of the same building block to yet other rings sizes (including a 12mer and a 13mer, accompanied by a minor amount of 14mer). This brings the total number of discrete foldamers that can be accessed from a single building block to five. For a single building block system to exhibit such highly diverse structure space is unique and sets this system of foldamers apart from proteins. Furthermore, the emergence of constitutional dynamicity opens up new avenues to foldamers with adaptive behavior.}, author = {Jin, Yulong and Mandal, Pradeep K and Wu, Juntian and Böcher, Niklas and Huc, Ivan and Otto, Sijbren}, issn = {1520-5126}, journal = {Journal of the American Chemical Society}, number = {5}, pages = {2822--2829}, publisher = {American Chemical Society}, title = {{(Re-)directing oligomerization of a single building block into two specific dynamic covalent foldamers through pH}}, doi = {10.1021/jacs.2c09325}, volume = {145}, year = {2023}, } @article{17074, abstract = {We verify Bogoliubov's approximation for translation invariant Bose gases in the mean field regime, i.e. we prove that the ground state energy EN is given by EN=NeH+infσ(H)+oN→∞(1), where N is the number of particles, eH is the minimal Hartree energy and H is the Bogoliubov Hamiltonian. As an intermediate result we show the existence of approximate ground states ΨN, i.e. states satisfying ⟨HN⟩ΨN=EN+oN→∞(1), exhibiting complete Bose--Einstein condensation with respect to one of the Hartree minimizers.}, author = {Brooks, Morris and Seiringer, Robert}, issn = {2690-1005}, journal = {Probability and Mathematical Physics}, number = {4}, pages = {939--1000}, publisher = {Mathematical Sciences Publishers}, title = {{Validity of Bogoliubov’s approximation fortranslation-invariant Bose gases}}, doi = {10.2140/pmp.2022.3.939}, volume = {3}, year = {2023}, } @article{17078, abstract = {For the emergence of life, the abiotic synthesis of RNA from its monomers is a central step. We found that in alkaline, drying conditions in bulk and at heated air‐water interfaces, 2′,3′‐cyclic nucleotides oligomerised without additional catalyst, forming up to 10‐mers within a day. The oligomerisation proceeded at a pH range of 7–12, at temperatures between 40–80 °C and was marginally enhanced by K+ ions. Among the canonical ribonucleotides, cGMP oligomerised most efficiently. Quantification was performed using HPLC coupled to ESI‐TOF by fitting the isotope distribution to the mass spectra. Our study suggests a oligomerisation mechanism where cGMP aids the incorporation of the relatively unreactive nucleotides C, A and U. The 2′,3′‐cyclic ribonucleotides are byproducts of prebiotic phosphorylation, nucleotide syntheses and RNA hydrolysis, indicating direct recycling pathways. The simple reaction condition offers a plausible entry point for RNA to the evolution of life on early Earth.}, author = {Dass, Avinash Vicholous and Wunnava, Sreekar and Langlais, Juliette and von der Esch, Beatriz and Krusche, Maik and Ufer, Lennard and Chrisam, Nico and Dubini, Romeo C. A. and Gartner, Florian and Angerpointner, Severin and Dirscherl, Christina F. and Rovo, Petra and Mast, Christof B. and Šponer, Judit E. and Ochsenfeld, Christian and Frey, Erwin and Braun, Dieter}, issn = {2570-4206}, journal = {ChemSystemsChem}, number = {1}, publisher = {Wiley}, title = {{RNA oligomerisation without added catalyst from 2′,3′‐cyclic nucleotides by drying at air-water interfaces}}, doi = {10.1002/syst.202200026}, volume = {5}, year = {2023}, } @article{17079, abstract = {We study moments of characteristic polynomials of truncated Haar distributed matrices from the three classical compact groups O(N), U(N) and Sp(2N). For finite matrix size we calculate the moments in terms of hypergeometric functions of matrix argument and give explicit integral representations highlighting the duality between the moment and the matrix size as well as the duality between the orthogonal and symplectic cases. Asymptotic expansions in strong and weak non-unitarity regimes are obtained. Using the connection to matrix hypergeometric functions, we establish limit theorems for the log-modulus of the characteristic polynomial evaluated on the unit circle.}, author = {Serebryakov, Alexander and Simm, Nick and Dubach, Guillaume}, issn = {2010-3271}, journal = {Random Matrices: Theory and Applications}, number = {01}, publisher = {World Scientific Publishing}, title = {{Characteristic polynomials of random truncations: Moments, duality and asymptotics}}, doi = {10.1142/s2010326322500496}, volume = {12}, year = {2023}, } @unpublished{17100, abstract = {Prophet inequalities are a central object of study in optimal stopping theory. A gambler is sent values online, sampled from an instance of independent distributions, in an adversarial, random or selected order, depending on the model. When observing each value, the gambler either accepts it as a reward or irrevocably rejects it and proceeds to observe the next value. The goal of the gambler, who cannot see the future, is maximising the expected value of the reward while competing against the expectation of a prophet (the offline maximum). In other words, one seeks to maximise the gambler-to-prophet ratio of the expectations. The model, in which the gambler selects the arrival order first, and then observes the values, is known as Order Selection. In this model a ratio of 0.7251 has been proved to be attainable for any instance. In very recent work, this has been improved up to 0.7258. If the gambler chooses the arrival order (uniformly) at random, we obtain the Random Order model. The worst case ratio over all possible instances has been extensively studied for at least 40 years. In the recent work aforementioned, through simulations, this ratio has been shown to be at most 0.7254 for the Random Order model, thus establishing for the first time that carefully choosing the order, instead of simply taking it at random, benefits the gambler. We give an alternative, more rigorous proof of this fact, by showing mathematically that in the Random Order model, no algorithm can achieve a ratio larger than 0.7235. This sets a new state-of-the-art hardness for this model, and establishes more formally that there is a real benefit in choosing the order.}, author = {Giambartolomei, Giordano and Frederik Mallmann-Trenn, Frederik Mallmann-Trenn and Saona Urmeneta, Raimundo J}, booktitle = {arXiv}, title = {{Prophet inequalities: Separating random order from order selection}}, doi = {10.48550/arXiv.2304.04024}, year = {2023}, } @article{17379, abstract = {We introduce a computational pipeline for simulating and designing C-shells, a new class of planar-to-spatial deployable linkage structures. A C-shell is composed of curved flexible beams connected at rotational joints that can be assembled in a stress-free planar configuration. When actuated, the elastic beams deform and the assembly deploys towards the target 3D shape. We propose two alternative computational design approaches for C-shells: (i) Forward exploration simulates the deployed shape from a planar beam layout provided by the user. Once a satisfactory overall shape is found, a subsequent design optimization adapts the beam geometry to reduce the elastic energy of the linkage while preserving the target shape. (ii) Inverse design is facilitated by a new geometric flattening method that takes a design surface as input and computes an initial layout of piecewise straight linkage beams. Our design optimization algorithm then calculates the smooth curved beams to best reproduce the target shape at minimal elastic energy. We find that C-shells offer a rich space for design and show several studies that highlight new shape topologies that cannot be achieved with existing deployable linkage structures.}, author = {Becker, Quentin and Suzuki, Seiichi and Ren, Yingying and Pellis, Davide and Panetta, Julian and Pauly, Mark}, issn = {1557-7368}, journal = {ACM Transactions on Graphics}, number = {6}, publisher = {Association for Computing Machinery}, title = {{C-shells: Deployable gridshells with curved beams}}, doi = {10.1145/3618366}, volume = {42}, year = {2023}, } @inbook{17380, abstract = {Deployable gridshells are a class of planar-to-spatial structures that achievea 3D curved geometry by inducing bending on a flat grid of elastic beams. However, theslender nature of these beams often conflicts with the structure’s load-bearing capacity.To address this issue, multiple layers are typically stacked to enhance out-of-planestiffness and prevent stability issues. The primary challenge then lies in deploying suchmulti-layered systems globally, as it requires significant shaping forces for actuation.This paper presents an alternative design approach that involves strategically connect-ing compact-to-volumetric gridshell components using weaving principles to shape athick segmented shell. This innovative approach allows for an incremental construc-tion process based entirely on deployable modules with volumetric configurations thatlocally provide the necessary structural depth for the entire system. To demonstrate thisprinciple, we present the realization of BamX, a research pavilion constructed usingdeployable cylindrical components made from raw bamboo slats. These componentsare interconnected at carefully optimized interlocking woven nodes, resulting in abending-active structural frame that is both strong and exceptionally lightweight. Todetermine the optimal topology and geometry of the pavilion, we employ an integrativecomputational approach that leverages advanced numerical optimization techniques.Our method incorporates a physics-based simulation of the bending and twisting be-havior of the bamboo ribbons. By finding the ideal locations for ribbon crossings, weensure that all external and internal forces are in global equilibrium while minimizingthe mechanical stress experienced by each ribbon. BamX exemplifies how a symbiosisof refined weaving craft and advanced computational modeling enables fascinatingnew opportunities for rethinking deployability in architecture.}, author = {Suzuki, Seiichi and Martin, Alison and Ren, Yingying and Chen, Tzu-Ying and Parascho, Stefana and Pauly, Mark}, booktitle = {Advances in Architectural Geometry 2023}, editor = {Dörfler, Kathrin and Knippers, Jan and Menges, Achim and Parascho, Stefana and Pottmann, Helmut and Wortmann, Thomas}, isbn = {9783111160115}, publisher = {De Gruyter}, title = {{BamX: Rethinking Deployability in Architecture through Weaving}}, doi = {10.1515/9783111162683-016}, year = {2023}, } @article{17381, abstract = {We present an algorithmic approach to discover, study, and design multistable elastic knots. Elastic knots are physical realizations of closed curves embedded in 3-space. When endowed with the material thickness and bending resistance of a physical wire, these knots settle into equilibrium states that balance the forces induced by elastic deformation and self-contacts of the wire. In general, elastic knots can have many distinct equilibrium states, i.e. they are multistable mechanical systems. We propose a computational pipeline that combines randomized spatial sampling and physics simulation to efficiently find stable equilibrium states of elastic knots. Leveraging results from knot theory, we run our pipeline on thousands of different topological knot types to create an extensive data set of multistable knots. By applying a series of filters to this data, we discover new transformable knots with interesting geometric and physical properties. A further analysis across knot types reveals geometric and topological patterns, yielding constructive principles that generalize beyond the currently tabulated knot types. We show how multistable elastic knots can be used to design novel deployable structures and engaging recreational puzzles. Several physical prototypes at different scales highlight these applications and validate our simulation.}, author = {Vidulis, Michele and Ren, Yingying and Panetta, Julian and Grinspun, Eitan and Pauly, Mark}, issn = {1557-7368}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {Association for Computing Machinery}, title = {{Computational exploration of multistable elastic knots}}, doi = {10.1145/3592399}, volume = {42}, year = {2023}, } @article{17382, abstract = {Elastic surfaces that morph between multiple geometrical configurations are of significant engineering value, with applications ranging from the deployment of space-based photovoltaic arrays, the erection of temporary shelters, and the realization of flexible display systems, to understanding the encapsulation and release of viral RNAs. In general, ensuring that a shape with a planar rest configuration can deploy into a target three-dimensional (3D) shape is a nontrivial problem. Moreover, it is difficult to physically realize the local deformations necessary to achieve such global transformation. Here, we give a tutorial on applying conformal mapping to rationalize the geometrical deformation of several microstructure designs. A conformal map is a function that locally preserves angles and shapes but not lengths: some regions are scaled (enlarged or shrunk) more than others. To transform a planar surface to 3D, we implement uniform local scalings as mechanical deformations. Numerous natural and architected material systems exhibit such behavior, including kirigami, origami, hydrogel, linkage mechanisms, and fabric membranes. The design and fabrication of conformally transformable surfaces is a transdisciplinary challenge involving insights from advanced manufacturing, computational design, material science, and mechanics. By recognizing that many material systems exhibit isotropic deformation, we hope to inspire researchers to adopt conformal mapping in designing next-generation surface-based engineering systems.}, author = {Wang, Yue and Ren, Yingying and Chen, Tian}, issn = {1528-9036}, journal = {Journal of Applied Mechanics}, number = {4}, publisher = {American Society of Mechanical Engineers}, title = {{From kirigami to hydrogels: A tutorial on designing conformally transformable surfaces}}, doi = {10.1115/1.4056350}, volume = {90}, year = {2023}, } @article{17498, abstract = {In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this paper, we take the first steps towards the goal of developing program logics for multi-language verification. Specifically, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.}, author = {Guéneau, Armaël and Hostert, Johannes and Spies, Simon and Sammler, Michael Joachim and Birkedal, Lars and Dreyer, Derek}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, number = {OOPSLA2}, pages = {716--744}, publisher = {Association for Computing Machinery}, title = {{Melocoton: A program logic for verified interoperability between OCaml and C}}, doi = {10.1145/3622823}, volume = {7}, year = {2023}, } @article{17499, abstract = {Much work in formal verification of low-level systems is based on one of two approaches: refinement or separation logic. These two approaches have complementary benefits: refinement supports the use of programs as specifications, as well as transitive composition of proofs, whereas separation logic supports conditional specifications, as well as modular ownership reasoning about shared state. A number of verification frameworks employ these techniques in tandem, but in all such cases the benefits of the two techniques remain separate. For example, in frameworks that use relational separation logic to prove contextual refinement, the relational separation logic judgment does not support transitive composition of proofs, while the contextual refinement judgment does not support conditional specifications. In this paper, we propose Conditional Contextual Refinement (or CCR, for short), the first verification system to not only combine refinement and separation logic in a single framework but also to truly marry them together into a unified mechanism enjoying all the benefits of refinement and separation logic simultaneously. Specifically, unlike in prior work, CCR’s refinement specifications are both conditional (with separation logic pre- and post-conditions) and transitively composable. We implement CCR in Coq and evaluate its effectiveness on a range of interesting examples.}, author = {Song, Youngju and Cho, Minki and Lee, Dongjae and Hur, Chung-Kil and Sammler, Michael Joachim and Dreyer, Derek}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, number = {POPL}, pages = {1121--1151}, publisher = {Association for Computing Machinery}, title = {{Conditional contextual refinement}}, doi = {10.1145/3571232}, volume = {7}, year = {2023}, } @article{17500, abstract = {Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions. Concretely, we present DimSum: a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators). We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.}, author = {Sammler, Michael Joachim and Spies, Simon and Song, Youngju and D'Osualdo, Emanuele and Krebbers, Robbert and Garg, Deepak and Dreyer, Derek}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, number = {POPL}, pages = {775--805}, publisher = {Association for Computing Machinery}, title = {{DimSum: A decentralized approach to multi-language semantics and verification}}, doi = {10.1145/3571220}, volume = {7}, year = {2023}, }