Refine
Year of publication
Document Type
- Preprint (666)
- Article (388)
- Working Paper (10)
- Part of Periodical (2)
- Conference Proceeding (1)
Has Fulltext
- yes (1067)
Is part of the Bibliography
- no (1067)
Keywords
- Heavy Ion Experiments (20)
- Hadron-Hadron Scattering (11)
- Hadron-Hadron scattering (experiments) (11)
- LHC (9)
- Lambda-Kalkül (8)
- Heavy-ion collision (6)
- Operationale Semantik (6)
- Programmiersprache (5)
- ALICE experiment (4)
- Collective Flow (4)
Institute
- Physik (1034)
- Frankfurt Institute for Advanced Studies (FIAS) (955)
- Informatik (931)
- Medizin (9)
- Geowissenschaften (7)
- Informatik und Mathematik (3)
- Georg-Speyer-Haus (2)
- Hochschulrechenzentrum (2)
- Biochemie und Chemie (1)
- Biowissenschaften (1)
This paper presents results from the "INUIT-JFJ/CLACE 2013" field campaign at the high alpine research station Jungfraujoch in January/February 2013. The chemical composition of ice particle residuals (IPR) in a size diameter range of 200–900 nm was measured in orographic, convective and non-convective clouds with a single particle mass spectrometer (ALABAMA) under ambient conditions characterized by temperatures between −28 and −4 °C and wind speed from 0.1 to 21 km h−1. Additionally, background aerosol particles in cloud free air were investigated. The IPR were sampled from mixed-phase clouds with two inlets which selectively extract small ice crystals in-cloud, namely the Counterflow Virtual Impactor (Ice-CVI) and the Ice Selective Inlet (ISI). The IPR as well as the aerosol particles were classified into seven different particle types: (1) black carbon, (2) organic carbon, (3) black carbon internally mixed with organic carbon, (4) minerals, (5) one particle group (termed "BioMinSal") that may contain biological particles, minerals, or salts, (6) industrial metals, and (7) lead containing particles. For any sampled particle population it was determined by means of single particle mass spectrometer how many of the analyzed particles belonged to each of these categories. Accordingly, between 20 and 30% of the IPR and roughly 42% of the background particles contained organic carbon. The measured fractions of minerals in the IPR composition varied from 6 to 33%, while the values for the "BioMinSal" group were between 15 and 29%. Four percent to 31% of the IPR contained organic carbon mixed with black carbon. Both inlets delivered similar results of the chemical composition and of the particle size distribution, although lead was found only in the IPR sampled by the Ice-CVI. The results show that the ice particle residual composition varies substantially between different cloud events, which indicates the influence of different meteorological conditions, such as origin of the air masses, temperature and wind speed.
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
Motivated by our experience in analyzing properties of translations between programming languages with observational semantics, this paper clarifies the notions, the relevant questions, and the methods, constructs a general framework, and provides several tools for proving various correctness properties of translations like adequacy and full abstractness. The presented framework can directly be applied to the observational equivalences derived from the operational semantics of programming calculi, and also to other situations, and thus has a wide range of applications.
Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analyzing translations between programming languages with respect to observational semantics. The behavior of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and mustconvergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extensions.
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
Background: School attendance during the COVID-19 pandemic is intensely debated.
Aim: In November 2020, we assessed SARS-CoV-2 infections and seroreactivity in 24 randomly selected school classes and connected households in Berlin, Germany.
Methods: We collected oro-nasopharyngeal swabs and blood samples, examining SARS-CoV-2 infection and IgG antibodies by RT-PCR and ELISA. Household members self-swabbed. We assessed individual and institutional prevention measures. Classes with SARS-CoV-2 infection and connected households were retested after 1 week.
Results: We examined 1,119 participants, including 177 primary and 175 secondary school students, 142 staff and 625 household members. SARS-CoV-2 infection occurred in eight classes, affecting each 1–2 individuals. Infection prevalence was 2.7% (95% confidence interval (CI): 1.2–5.0; 9/338), 1.4% (95% CI: 0.2–5.1; 2/140), and 2.3% (95% CI: 1.3–3.8; 14/611) among students, staff and household members. Six of nine infected students were asymptomatic at testing. We detected IgG antibodies in 2.0% (95%CI: 0.8–4.1; 7/347), 1.4% (95% CI: 0.2–5.0; 2/141) and 1.4% (95% CI: 0.6–2.7; 8/576). Prevalence increased with inconsistent facemask-use in school, walking to school, and case-contacts outside school. For three of nine households with infection(s), origin in school seemed possible. After 1 week, no school-related secondary infections appeared in affected classes; the attack rate in connected households was 1.1%.
Conclusion: School attendance under rigorously implemented preventive measures seems reasonable. Balancing risks and benefits of school closures need to consider possible spill-over infection into households. Deeper insight is required into the infection risks due to being a schoolchild vs attending school.