| 1. |
|
|
| 2. |
|
|
| 3. |
- Aamodt, K., et al.
(författare)
-
The ALICE experiment at the CERN LHC
- 2008
-
Ingår i: Journal of Instrumentation. - 1748-0221. ; 3:S08002
-
Forskningsöversikt (refereegranskat)abstract
- ALICE (A Large Ion Collider Experiment) is a general-purpose, heavy-ion detector at the CERN LHC which focuses on QCD, the strong-interaction sector of the Standard Model. It is designed to address the physics of strongly interacting matter and the quark-gluon plasma at extreme values of energy density and temperature in nucleus-nucleus collisions. Besides running with Pb ions, the physics programme includes collisions with lighter ions, lower energy running and dedicated proton-nucleus runs. ALICE will also take data with proton beams at the top LHC energy to collect reference data for the heavy-ion programme and to address several QCD topics for which ALICE is complementary to the other LHC detectors. The ALICE detector has been built by a collaboration including currently over 1000 physicists and engineers from 105 Institutes in 30 countries, Its overall dimensions are 16 x 16 x 26 m(3) with a total weight of approximately 10 000 t. The experiment consists of 18 different detector systems each with its own specific technology choice and design constraints, driven both by the physics requirements and the experimental conditions expected at LHC. The most stringent design constraint is to cope with the extreme particle multiplicity anticipated in central Pb-Pb collisions. The different subsystems were optimized to provide high-momentum resolution as well as excellent Particle Identification (PID) over a broad range in momentum, up to the highest multiplicities predicted for LHC. This will allow for comprehensive studies of hadrons, electrons, muons, and photons produced in the collision of heavy nuclei. Most detector systems are scheduled to be installed and ready for data taking by mid-2008 when the LHC is scheduled to start operation, with the exception of parts of the Photon Spectrometer (PHOS), Transition Radiation Detector (TRD) and Electro Magnetic Calorimeter (EMCal). These detectors will be completed for the high-luminosity ion run expected in 2010. This paper describes in detail the detector components as installed for the first data taking in the summer of 2008.
|
|
| 4. |
- Blanchette, Jasmin Christian, et al.
(författare)
-
Encoding Monomorphic and Polymorphic Types
- 2013
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642367410 ; 7795, s. 493-507
-
Konferensbidrag (refereegranskat)abstract
- Most automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of “cover”. The new encodings are implemented, and partly proved correct, in Isabelle/HOL. Our evaluation finds them vastly superior to previous schemes.
|
|
| 5. |
- Blanchette, Jasmin Christian, et al.
(författare)
-
Encoding monomorphic and polymorphic types
- 2016
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 12:4
-
Tidskriftsartikel (refereegranskat)abstract
- Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 po lymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of “cover”. The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.
|
|
| 6. |
- Gengelbach, Arve
(författare)
-
Conservative Definitions for Higher-order Logic with Ad-hoc Overloading
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- With an ever growing dependency on computer systems, the need to guarantee their correct behaviour increases. Mathematically rigorous techniques like formal verification offer a way to derive a system's mathematical properties for example with the help of a theorem prover. A theorem prover is a type of software that assists a user in deriving theorems expressed in a formal language. With a theorem prover one should never be able to prove something that is contradictory, as otherwise the proof effort is worthless. This property is called consistency and is essential for formal developments.Theorem provers enjoy high confidence, since they often rely on a trusted logical kernel that is enriched with new symbols in a controlled way. Instead of asserting the existence of mathematical objects with their desired properties, new symbols are introduced through definitions. These definitions are checked by this kernel, and expected to act as abbreviations. Any theorem that is expressible without a definition should not need that definition in its proof. A definition satisfying this property is called conservative. Conservative definitions are especially important as they preserve consistency, so that a proof of a contradiction is not possible after adding these definitions.Isabelle/HOL is a prominent theorem prover with the unique feature of permitting different definitions of one constant at non-overlapping types. In addition to these so-called overloading definitions, a symbol may be used before it is defined. These features mean that consistency or conservativity arguments for simpler logics do not immediately apply to Isabelle/HOL. In the past, design flaws in the definitional mechanism made theories in the Isabelle/HOL theorem prover inconsistent, e.g. it was possible to derive a contradiction from cyclic definitions.With this thesis we show that (overloading) definitions in higher-order logic (HOL) are conservative, hence not source of inconsistency. We define and prove a notion of conservativity that applies to theories of overloading definitions in higher-order logic and formalise aspects of our results in a theorem prover. As a practical implication, when searching for a proof of a formula, our syntactic conservativity criterion allows to exclude irrelevant symbols. In particular, our results confirm that Isabelle/HOL theories are consistent, thus users cannot introduce contradictions through definitions. As a specialisation of our work, our notion of conservativity holds for variants of HOL without overloading. Overall, our work contributes to the understanding of higher-order logic with overloading definitions.
|
|
| 7. |
- Guillou, Liane, et al.
(författare)
-
Findings of the 2016 WMT Shared Taskon Cross-lingual Pronoun Prediction
- 2016
-
Ingår i: Proceedings of the First Conference on Machine Translation. ; , s. 525-542
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- We describe the design, the evaluation setup, and the results of the 2016 WMT shared task on cross-lingual pronoun prediction. This is a classification task in which participants are asked to provide predictions on what pronoun class label should replace a placeholder value in the target-language text, provided in lemmatised and PoS-tagged form. We provided four subtasks, for the English–French and English–German language pairs, in both directions. Eleven teams participated in the shared task; nine for the English–French subtask, five for French–English, nine for English–German, and six for German–English. Most of the submissions outperformed two strong language-model-based baseline systems, with systems using deep recurrent neural networks outperforming those using other architectures for most language pairs.
|
|
| 8. |
- Pellen, Mathieu, et al.
(författare)
-
Angular coefficients in W + j production at the LHC with high precision
- 2022
-
Ingår i: European Physical Journal C. - : Springer Science and Business Media LLC. - 1434-6044 .- 1434-6052. ; 82:8
-
Tidskriftsartikel (refereegranskat)abstract
- The extraction of the W-boson mass, a fundamental parameter of the Standard Model, from hadron-hadron collision requires precise theory predictions. In this regard, angular coefficients are crucial to model the dynamics of W-boson production. In this work, we provide, for the first time, angular coefficients at NNLO QCD + NLO EW accuracy for finite transverse momentum W-boson at the LHC. The corrections can reach up to 10 % in certain regions of phase space. They are accompanied by a significant reduction of the scale uncertainty. This work should, besides providing reference values for theory-data comparison, provide state-of-the-art theory input for W-boson mass measurements.
|
|
| 9. |
|
|
| 10. |
|
|
| 11. |
|
|
| 12. |
|
|
| 13. |
- Aad, G., et al.
(författare)
-
- 2010
-
swepub:Mat__t
|
|
| 14. |
- Aad, G., et al.
(författare)
-
- 2011
-
swepub:Mat__t
|
|
| 15. |
- Aad, G., et al.
(författare)
-
- 2010
-
swepub:Mat__t
|
|
| 16. |
- Aad, G., et al.
(författare)
-
- 2010
-
swepub:Mat__t
|
|
| 17. |
- Aad, G., et al.
(författare)
-
- 2010
-
swepub:Mat__t
|
|
