Refine
Year of publication
Document Type
- Preprint (669)
- Article (368)
- Working Paper (8)
- Conference Proceeding (2)
Language
- English (1047)
Has Fulltext
- yes (1047)
Is part of the Bibliography
- no (1047)
Keywords
- Heavy Ion Experiments (20)
- Hadron-Hadron Scattering (11)
- Hadron-Hadron scattering (experiments) (11)
- LHC (9)
- Heavy-ion collision (6)
- ALICE experiment (4)
- Collective Flow (4)
- Jets (4)
- Lambda-Kalkül (4)
- Quark-Gluon Plasma (4)
- semantics (4)
- ALICE (3)
- Heavy Ions (3)
- Jets and Jet Substructure (3)
- contextual equivalence (3)
- lambda calculus (3)
- pp collisions (3)
- Beauty production (2)
- Charm physics (2)
- Experimental nuclear physics (2)
- Experimental particle physics (2)
- Formale Semantik (2)
- Heavy Quark Production (2)
- Kontextuelle Gleichheit (2)
- Lepton-Nucleon Scattering (experiments) (2)
- Operationale Semantik (2)
- Particle Correlations and Fluctuations (2)
- Particle and resonance production (2)
- Particle correlations and fluctuations (2)
- Pb–Pb collisions (2)
- Programmiersprache (2)
- QCD (2)
- Single electrons (2)
- brain metastases (2)
- breast cancer (2)
- letrec (2)
- 900 GeV (1)
- ALICE detector (1)
- Anti-nuclei (1)
- Atherosclerosis (1)
- Boosted Jets (1)
- Cardiovascular diseases (1)
- Centrality Class (1)
- Centrality Selection (1)
- Collective Flow, (1)
- Comparison with QCD (1)
- Diagnostic tests (1)
- Electron-pion identification (1)
- Electroweak interaction (1)
- Elliptic flow (1)
- FOS: Physical sciences (1)
- Femtoscopy (1)
- Fibre/foam sandwich radiator (1)
- Germany (1)
- HBT (1)
- Hadron production (1)
- Hadron-Hadron Scattering Heavy (1)
- Hadron-hadron interactions (1)
- Hard Scattering (1)
- Health risk analysis (1)
- Heavy Ion Experiment (1)
- Heavy flavor production (1)
- Heavy flavour production (1)
- Heavy ions (1)
- Heavy-flavour decay muons (1)
- Heavy-flavour production (1)
- Heavy-ion collisions (1)
- Hepatitis C (1)
- Hepatitis C antibodies (1)
- Hepatitis C antigens (1)
- High Energy Physics - Lattice (hep-lat) (1)
- High Energy Physics - Phenomenology (hep-ph) (1)
- High Energy Physics - Theory (hep-th) (1)
- Immunoassay (1)
- Inclusive spectra (1)
- Intensity interferometry (1)
- Invariant Mass Distribution (1)
- Ionisation energy loss (1)
- Italy (1)
- Jet Physics (1)
- Jet Substructure (1)
- Material budget (1)
- Mid-rapidity (1)
- Minimum Bias (1)
- Monte Carlo (1)
- Multi-Parton Interactions (1)
- Multi-strange baryons (1)
- Multi-wire proportional drift chamber (1)
- Myocardial infarction (1)
- Neural network (1)
- Nichtdeterminismus (1)
- Nuclear Theory (nucl-th) (1)
- Nuclear modification factor (1)
- PYTHIA (1)
- Particle and Resonance Production (1)
- Pb–Pb (1)
- Production Cross Section (1)
- Properties of Hadrons (1)
- Proton–proton (1)
- Quark Deconfinement (1)
- Quark Gluon Plasma (1)
- Quark Production (1)
- Quark gluon plasma (1)
- Quarkonium (1)
- Rapidity Range (1)
- Relativistic heavy ion physics (1)
- Relativistic heavy-ion collisions (1)
- Resolution Parameter (1)
- Single muons (1)
- Stroke (1)
- Sweden (1)
- Systematic Uncertainty (1)
- TR (1)
- Time Projection Chamber (1)
- Tracking (1)
- Transition radiation detector (1)
- Transverse momentum (1)
- Trigger (1)
- Vector Boson Production (1)
- Xenon-based gas mixture (1)
- asymptomatic (1)
- bisimulation (1)
- call-by-need (1)
- dE/dx (1)
- detector (1)
- experimental results (1)
- heavy ion experiments (1)
- non-determinism (1)
- nondeterminism (1)
- prognostic scores (1)
- programming languages (1)
- quark gluon plasma (1)
- simulation (1)
- spectra (1)
- √sN N = 2.76 TeV (1)
Institute
- Physik (1031)
- Frankfurt Institute for Advanced Studies (FIAS) (959)
- Informatik (934)
- Medizin (4)
- Informatik und Mathematik (3)
- Hochschulrechenzentrum (2)
- Biochemie und Chemie (1)
- Geowissenschaften (1)
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus’ semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as nondeterminism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe’s proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.
This paper shows equivalence of several versions of applicative similarity and contextual approximation, and hence also of applicative bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seq-operator. LR models an untyped version of the core language of Haskell. The use of bisimilarities simplifies equivalence proofs in calculi and opens a way for more convenient correctness proofs for program transformations. The proof is by a fully abstract and surjective transfer into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of our similarities and contextual approximation can be shown by Howe's method. Similarity is transferred back to LR on the basis of an inductively defined similarity. The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite trees which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, which is also an identity on letrec-free expressions.
This paper shows equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seqoperator. LR models an untyped version of the core language of Haskell. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations.
The proof is by a fully abstract and surjective transfer of the contextual approximation into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of similarity and contextual approximation can be shown by Howe's method. Using an equivalent but inductive definition of behavioral preorder we then transfer similarity back to the calculus LR.
The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite tress, which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, and also with a call-by-need letrec calculus with a less complex definition of reduction than LR.
Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
Our motivation is the question whether the lazy lambda calculus, a pure lambda calculus with the leftmost outermost rewriting strategy, considered under observational semantics, or extensions thereof, are an adequate model for semantic equivalences in real-world purely functional programming languages, in particular for a pure core language of Haskell. We explore several extensions of the lazy lambda calculus: addition of a seq-operator, addition of data constructors and case-expressions, and their combination, focusing on conservativity of these extensions. In addition to untyped calculi, we study their monomorphically and polymorphically typed versions. For most of the extensions we obtain non-conservativity which we prove by providing counterexamples. However, we prove conservativity of the extension by data constructors and case in the monomorphically typed scenario.
This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models.We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.
This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky’s lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky’s lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models. We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen. 1998 ACM Subject Classification: F.4.2, F.3.2, F.3.3, F.4.1. Key words and phrases: semantics, contextual equivalence, bisimulation, lambda calculus, call-by-need, letrec.
This note shows that in non-deterministic extended lambda calculi with letrec, the tool of applicative (bi)simulation is in general not usable for contextual equivalence, by giving a counterexample adapted from data flow analysis. It also shown that there is a flaw in a lemma and a theorem concerning finite simulation in a conference paper by the first two authors.
This paper shows equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seqoperator. LR models an untyped version of the core language of Haskell. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations.
The proof is by a fully abstract and surjective transfer of the contextual approximation into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of similarity and contextual approximation can be shown by Howe's method. Using an equivalent but inductive definition of behavioral preorder we then transfer similarity back to the calculus LR.
The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite tress, which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, and also with a call-by-need letrec calculus with a less complex definition of reduction than LR.
Background: The diagnostic accuracy of the Elecsys® HCV Duo antigen-antibody combination immunoassay (Roche Diagnostics GmbH) was evaluated for the detection of hepatitis C virus (HCV) infection, versus commercially available comparators.
Methods: This multicenter study (August 2020–March 2021) assessed the specificity of the Elecsys HCV Duo immunoassay and comparator assays in blood donor and routine clinical laboratory samples; sensitivity was determined in confirmed HCV-positive samples and seroconversion panels. The Elecsys HCV Duo immunoassay was compared with the Monolisa HCV Ag-Ab ULTRA V2, Murex HCV Ag/Ab Combination and ARCHITECT HCV Ag assays, as well as nucleic acid testing (NAT). The antibody (anti-HCV) module of the Elecsys HCV Duo immunoassay was compared with the Elecsys Anti-HCV II, Alinity s Anti-HCV, ARCHITECT Anti-HCV and RIBA HCV 3.0 SIA assays.
Results: The specificity of the Elecsys HCV Duo immunoassay was 99.94% (95% confidence interval [CI], 99.89–99.97) and 99.92% (95% CI, 99.71–99.99) in blood donor (n = 20,634) and routine clinical laboratory samples (n = 2531), respectively. The specificity of the Elecsys HCV Duo immunoassay was similar or better than comparator assays. The sensitivity of the Elecsys HCV Duo immunoassay in confirmed HCV-positive samples (n = 257) was 99.6%. In seroconversion panels, the Elecsys HCV Duo immunoassay detected infections earlier (2.2–21.9 days) than all but one of the comparator assays and detected HCV 1.8 days later than NAT.
Conclusions: The Elecsys HCV Duo immunoassay shows high diagnostic accuracy, reduces the diagnostic window, and could be used when NAT is not possible.
Phase transitions in a non-perturbative regime can be studied by ab initio Lattice Field Theory methods. The status and future research directions for LFT investigations of Quantum Chromo-Dynamics under extreme conditions are reviewed, including properties of hadrons and of the hypothesized QCD axion as inferred from QCD topology in different phases. We discuss phase transitions in strong interactions in an extended parameter space, and the possibility of model building for Dark Matter and Electro-Weak Symmetry Breaking. Methodological challenges are addressed as well, including new developments in Artificial Intelligence geared towards the identification of different phases and transitions.
The three-dimensional structure determination of RNAs by NMR spectroscopy relies on chemical shift assignment, which still constitutes a bottleneck. In order to develop more efficient assignment strategies, we analysed relationships between sequence and 1H and 13C chemical shifts. Statistics of resonances from regularly Watson– Crick base-paired RNA revealed highly characteristic chemical shift clusters. We developed two approaches using these statistics for chemical shift assignment of double-stranded RNA (dsRNA): a manual approach that yields starting points for resonance assignment and simplifies decision trees and an automated approach based on the recently introduced automated resonance assignment algorithm FLYA. Both strategies require only unlabeled RNAs and three 2D spectra for assigning the H2/C2, H5/C5, H6/C6, H8/C8 and H10/C10 chemical shifts. The manual approach proved to be efficient and robust when applied to the experimental data of RNAs with a size between 20 nt and 42 nt. The more advanced automated assignment approach was successfully applied to four stemloop RNAs and a 42 nt siRNA, assigning 92–100% of the resonances from dsRNA regions correctly. This is the first automated approach for chemical shift assignment of non-exchangeable protons of RNA and their corresponding 13C resonances, which provides an important step toward automated structure determination of RNAs.
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus' semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as non-determinism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe's proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.
In order to quantitatively analyse the chemical and dynamical evolution of the polar vortex it has proven extremely useful to work with coordinate systems that follow the vortex flow. We propose here a two-dimensional quasi-Lagrangian coordinate system {X i, delta X i}, based on the mixing ratio of a long-lived stratospheric trace gas i, and its systematic use with i = N2O, in order to describe the structure of a well-developed Antarctic polar vortex. In the coordinate system {X i, delta X i} the mixing ratio X i is the vertical coordinate and delta X i = X i(theta) - X i vort(theta) is the meridional coordinate (X i vort(theta) being a vertical reference profile in the vortex core). The quasi-Lagrangian coordinates {X i, delta X i} persist for much longer time than standard isentropic coordinates, potential temperature theta and equivalent latitude Phi e, do not require explicit reference to geographic space, and can be derived directly from high-resolution in situ measurements. They are therefore well-suited for studying the evolution of the Antarctic polar vortex throughout the polar winter with respect to the relevant chemical and microphysical processes. By using the introduced coordinate system {X N2O, delta X N2O} we analyze the well-developed Antarctic vortex investigated during the APE-GAIA (Airborne Polar Experiment – Geophysica Aircraft in Antarctica – 1999) campaign (Carli et al., 2000). A criterion, which uses the local in-situ measurements of X i=X i(theta) and attributes the inner vortex edge to a rapid change (delta-step) in the meridional profile of the mixing ratio X i, is developed to determine the (Antarctic) inner vortex edge. In turn, we suggest that the outer vortex edge of a well-developed Antarctic vortex can be attributed to the position of a local minimum of the X H2O gradient in the polar vortex area. For a well-developed Antarctic vortex, the delta X N2O-parametrization of tracer-tracer relationships allows to distinguish the tracer inter-relationships in the vortex core, vortex boundary region and surf zone and to examine their meridional variation throughout these regions. This is illustrated by analyzing the tracer-tracer relationships X i : X N2O obtained from the in-situ data of the APE-GAIA campaign for i = CFC-11, CFC-12, H-1211 and SF6. A number of solitary anomalous points in the CFC-11 : N2O correlation, observed in the Antarctic vortex core, are interpreted in terms of small-scale cross-isentropic dispersion.
Aims: Carotid intima media thickness (CIMT) predicts cardiovascular (CVD) events, but the predictive value of CIMT change is debated. We assessed the relation between CIMT change and events in individuals at high cardiovascular risk.
Methods and results: From 31 cohorts with two CIMT scans (total n = 89070) on average 3.6 years apart and clinical follow-up, subcohorts were drawn: (A) individuals with at least 3 cardiovascular risk factors without previous CVD events, (B) individuals with carotid plaques without previous CVD events, and (C) individuals with previous CVD events. Cox regression models were fit to estimate the hazard ratio (HR) of the combined endpoint (myocardial infarction, stroke or vascular death) per standard deviation (SD) of CIMT change, adjusted for CVD risk factors. These HRs were pooled across studies.
In groups A, B and C we observed 3483, 2845 and 1165 endpoint events, respectively. Average common CIMT was 0.79mm (SD 0.16mm), and annual common CIMT change was 0.01mm (SD 0.07mm), both in group A. The pooled HR per SD of annual common CIMT change (0.02 to 0.43mm) was 0.99 (95% confidence interval: 0.95–1.02) in group A, 0.98 (0.93–1.04) in group B, and 0.95 (0.89–1.04) in group C. The HR per SD of common CIMT (average of the first and the second CIMT scan, 0.09 to 0.75mm) was 1.15 (1.07–1.23) in group A, 1.13 (1.05–1.22) in group B, and 1.12 (1.05–1.20) in group C.
Conclusions: We confirm that common CIMT is associated with future CVD events in individuals at high risk. CIMT change does not relate to future event risk in high-risk individuals.
The vector U bosons, or so-called “dark photons,” are one of the possible candidates for the dark matter mediators. They are supposed to interact with the standard matter via a “vector portal” due to the Uð1Þ − Uð1Þ0 symmetry group mixing which might make them visible in particle and heavy-ion experiments. While there is no confirmed observation of dark photons, the detailed analysis of different experimental data allows to estimate the upper limit for the kinetic mixing parameter ϵ2 depending on the mass MU of U bosons which is also unknown. In this study we present theoretical constraints on the upper limit of ϵ2ðMUÞ in the mass range MU ≤ 0.6 GeV from the comparison of the calculated dilepton spectra with the experimental data from the HADES collaboration at SIS18 energies where the dark photons are not observed. Our analysis is based on the microscopic Parton-Hadron-String Dynamics (PHSD) transport
approach which reproduces well the measured dilepton spectra in p þ p, p þ A and A þ A collisions. Additionally to the different dilepton channels originating from interactions and decays of ordinary matter particles (mesons and baryons), we incorporate the decay of hypothetical U bosons to dileptons, U → eþe−, where the U bosons themselves are produced by the Dalitz decay of pions π0 → γU, η mesons η → γU and Delta resonances Δ → NU. Our analysis can help to estimate the requested accuracy for future experimental searches of “light” dark photons by dilepton experiments.
Lattice strains of appropriate symmetry have served as an excellent tool to explore the interaction of superconductivity in the iron-based superconductors with nematic and stripe spin-density wave (SSDW) order, which are both closely tied to an orthorhombic distortion. In this work, we contribute to a broader understanding of the coupling of strain to superconductivity and competing normal-state orders by studying CaKFe4As4 under large, in-plane strains of B1g and B2g symmetry. In contrast to the majority of iron-based superconductors, pure CaKFe4As4 exhibits superconductivity with relatively high transition temperature of Tc∼35 K in proximity of a non-collinear, tetragonal, hedgehog spin-vortex crystal (SVC) order. Through experiments, we demonstrate an anisotropic in-plane strain response of Tc, which is reminiscent of the behavior of other pnictides with nematicity. However, our calculations suggest that in CaKFe4As4, this anisotropic response correlates with the one of the SVC fluctuations, highlighting the close interrelation of magnetism and high-Tc superconductivity. By suggesting moderate B2g strains as an effective parameter to change the stability of SVC and SSDW, we outline a pathway to a unified phase diagram of iron-based superconductivity.