Portail HAL-PSL
Not a member yet
293219 research outputs found
Sort by
Supramolecular rotaxanes and polyrotaxanes as potential MRI contrast agents: a comprehensive 17O NMR and relaxometric study
No full textInternational audienceRotaxanes and polyrotaxanes made of substituted cyclodextrins (CDs) were designed as potential MRI contrast agents or bimodal optical and MRI probes. After characterization of the threading kinetics and the exact composition of the polyrotaxanes, their MRI properties have been investigated by 1 H relaxometry and 17 O NMR. We demonstrated that the relaxivity of these systems is increasing with increasing size (modified CDs, rotaxanes, and polyrotaxanes). 17 O NMR studies show that the various systems have similar water exchange rates, in the same range as that of Gd-DOTA-monoamide complexes. Interestingly, NMRD data of the smaller systems can be only analyzed by considering both local and global motions via Lipari-Szabo approach, underlining the importance of internal flexibility. On the other hand, the disubsituted rotaxane and the polyrotaxanes are highly rigid and can be characterized with a single rotational correlation time. Their relaxivity is considerably enhanced by a second sphere contribution which is strongly dependent on the structure. It increases from the rotaxane to the mono-and the disubstituted polyrotaxanes, and as expected, it diminishes with decreasing coverage of the axle. The fundamental understanding provided by this comprehensive study will help the design of versatile and more efficient supramolecular interlocked systems such as rotaxanes and polyrotaxanes for MRI applications.</div
Apprehensions of illiberalism. Examining how the principles of the Rule of Law are dismantled
No full textInternational audienc
Milankovitch forcing of equilibrium ground-ice on Mars
No full textInternational audienceExchangeable ice deposits are present today on the surface of Mars in polar caps and in the shallow subsurface in mid-latitudes. Geologic observations indicate these deposits waxed and waned in the past, at times, along with the emplacement and loss of equatorial glaciers. Here, we couple a climate model with an ice stability criterion, to self-consistently determine the distribution of the mid-latitude ground-ice deposits in di!usive equilibrium with the atmosphere, at present and under past orbital configurations. This new coupling and iteration between the short-term and long-term models improves upon past calculations that do not allow the ice table to evolve over timescales much longer than the annual climate dynamics. The model predictions for the extent of the equilibrium ice-table in the past match the latitudinal distribution of terrain softening geologic features previously mapped. At past times, thermally stable shallow ground ice is expected even in equatorial regions, in parts of Tharsis and Arabia Terra.</div
Keep Singing the Gospel
No full textInternational audienceGospel is a strongly typed, contract based specification language for OCaml. Gospel aims to be a lightweight surface syntax for Separation Logic formulae that can be used to specify arbitrary values. It is meant to be general enough that it may be used in conjunction with whatever verification environment (or environments) the programmer prefers. Although Gospel has already been presented in previous publications, we have made improvements to its semantics, type systems and tooling ecosystem that are worth reporting on. We present these through a series of examples and their translation into GospelSL, an intermediate Separation Logic that we use to define the semantics of Gospel. From GospelSL, we show how we can automatically create a Rocq file that enables verification using CFML or Iris
Tacq -Context Aware Tactic Recommendation for Rocq
No full textInternational audienceDespite recent impressive achievements of Large Language Models (LLMs) in formal mathematics using proof assistants, the state-of-the-art has mostly focused on mathematics competitions where problems typically involve simple and well-understood concepts. This is unfortunately far from current practice in formal mathematics, where experts must navigate large libraries of lemmas and manipulate complex constructions.In this paper, we focus on the problem of next tactic recommendation for Rocq. A key issue is to prompt the model with enough context to understand the current goal when the proof relies on large libraries with numerous dependencies and where specialized notations are pervasive. We present a tool that can extract notations and dependencies from the current goal and annotate them with natural language docstrings. We show that such augmented contexts improve the ability of state-of-the-art models to generate valid tactics on the challenging MathComp library.</p
Vers une évaluation hyper-moderne des politiques publiques
No full textNational audienceDepuis son origine en contexte public, l’évaluation des politiques a connu différentes formes. D’abord, une évaluation qualifiée d’« administrative », inscrite dans une logique hiérarchique et centrée sur la conformité procédurale. Ensuite, une évaluation « managériale » portée par les principes du New Public Management (NPM), valorisant la performance, la responsabilisation individuelleet l’usage d’indicateurs quantitatifs. Enfin, une évaluation plus « collaborative et ouverte », intégrant la réflexivité, la participation et la prise en compte du contexte social et territorial de l’action publique, en intégrant des approches post-NPM, plus récentes. Pourtant, malgré ces évolutions, l’évaluation des politiques publiques est actuellement critiquée, que cela soit sur le plan conceptuel ou sur celui plus pratique. Une évaluation renouvelée semble alors nécessaire !
Search for an eV-scale sterile neutrino with the first six detection units of KM3NeT/ORCA
No full textInternational audienceThe existence of an eV-scale sterile neutrino has been proposed to explain several anomalous experimental results obtained over the course of the past 25 years. The first search for such a sterile neutrino conducted with data from KM3NeT/ORCA -- a water Cherenkov neutrino telescope under construction at the bottom of the Mediterranean Sea -- is reported in this paper. GeV-scale atmospheric neutrino oscillations are measured by reconstructing the energy and arrival direction of up-going neutrinos that have traversed the Earth. This study is based on a data sample containing 5828 neutrino candidates collected with 6 detection units ( of the complete detector), corresponding to an exposure of 433 kton-years. From the expected effect of an eV-scale sterile neutrino on the first standard oscillation maximum, simultaneous constraints are put on the magnitude of the and mixing elements under the assumption eV. The results are compatible with the absence of mixing between active neutrinos and a sterile state, with and at a confidence level. Such constraints are compatible with the results reported by other long-baseline experiments, and indicate that with KM3NeT/ORCA it is possible to bring crucial contributions to sterile neutrino searches in the coming years
Interhemispheric and Latitudinal Variability of Ionospheric Disturbances During the 19-20 December 2015 Geomagnetic Storm: Insights from the South American Sector
No full textInternational audienceThis study investigates the response of the South American ionosphere to the December 19-20, 2015, geomagnetic storm using multi-instrument satellite and ground-based data. An interplanetary shock triggered prompt penetration electric fields (PPEFs) during the storm's initial phase, initiating rapid DP2 currents and significant equatorial electrojet (EEJ) fluctuations, particularly in Jicamarca, Peru. Our analysis shows that dayside field-aligned currents (FACs) are the primary drivers of the observed DP2 fluctuations. The South Atlantic Magnetic Anomaly (SAMA) also induced a westward geomagnetic gradient-induced current at the equatorward boundary, which suppressed the EEJ current at São Luiz during the magnetically quiet period. During the storm's main phase, eastward PPEFs enhanced ionospheric irregularities at several Global Positioning Satellite (GPS) stations: Sao Luiz (14.8%), Cuiaba (11.4%), and Jatai (15.5%) in Brazil; Tucuma (33.6%) and Rio Grande (33.2%) in Argentina; and all Peruvian GPS stations (5.8 -57.6%), with Arequipa showing the highest percentage. Conversely, irregularities were inhibited at Eusebio (-31.5%), São José dos Campos (-11.8%), and Campo Grande (-4.8%) in Brazil, and Rosario (-9.4%) and Villegas (-0.8%) in Argentina, relative to a magnetically quiet day, which was attributed to the interplay between westward disturbance dynamo electric fields (DDEF) and PPEF. Joule heating, peaking at 14:35 UT on 20 December drove equatorward disturbance winds that generated the DDEF and modulated irregularities during the recovery phase. Westward DDEF suppressed post-sunset irregularities across most Brazilian and Argentine stations (-50.2% to -10.1%), but slightly enhanced post-midnight ionospheric irregularities at Cuiabá (+4.3%) and Tucuma (+21.1%). All Peruvian stations recorded post-midnight enhancements (+14.8% to +136.7%), with Arequipa showing the highest increase. We quantified the delayed magnetic response of the disturbance dynamo (Ddyn) relative to Joule heating, revealing propagation delays of approximately 6, 8.5, and 8.2 h in Brazil, Argentina, and Peru, respectively. Ddyn exhibited strong spatiotemporal variability, including spatial anomalies associated with the SAMA. The Peruvian sector dominated the Ddyn power (59.0%), followed by Brazil (35.1%) and Argentina (5.9%). Evidence of interhemispheric FAC asymmetry, attributed to seasonal variability, was also observed. These findings significantly advance our understanding of storm-time lowlatitude electrodynamics and their regional variability