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.