Refine
Year of publication
Document Type
- Preprint (673)
- Article (402)
- Working Paper (10)
- Conference Proceeding (3)
- Doctoral Thesis (1)
Has Fulltext
- yes (1089)
Is part of the Bibliography
- no (1089)
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)
- Jets (4)
- Quark-Gluon Plasma (4)
- ALICE (3)
- Heavy Ions (3)
- Jets and Jet Substructure (3)
- Nebenläufigkeit (3)
- pp collisions (3)
- Beauty production (2)
- Charm physics (2)
- Experimental nuclear physics (2)
- Experimental particle physics (2)
- Funktionale Programmiersprache (2)
- Heavy Quark Production (2)
- Lepton-Nucleon Scattering (experiments) (2)
- Particle Correlations and Fluctuations (2)
- Particle and resonance production (2)
- Particle correlations and fluctuations (2)
- Pb–Pb collisions (2)
- Pufferspeicher (2)
- QCD (2)
- Single electrons (2)
- 900 GeV (1)
- ALICE detector (1)
- Alice ML (1)
- Anti-nuclei (1)
- Bacteraemia (1)
- Berufliche Gesundheit (1)
- Berufszufriedenheit (1)
- Betriebliche Gesundheitsförderung (1)
- Bloodstream infections (1)
- Boosted Jets (1)
- Büroarbeit (1)
- CVID (1)
- Cancer models (1)
- Centrality Class (1)
- Centrality Selection (1)
- Cognitive impairment (1)
- Collective Flow, (1)
- Comparison with QCD (1)
- Contextual Equivalence (1)
- Dance (1)
- Dehntraining (1)
- Electron-pion identification (1)
- Electroweak interaction (1)
- Elliptic flow (1)
- European Society for Immunodeficiencies (ESID) (1)
- Extracorporeal devices (1)
- FOS: Physical sciences (1)
- Femtoscopy (1)
- Fibre/foam sandwich radiator (1)
- First-line regimen (1)
- Five-Konzept (1)
- Futures (1)
- Genetic engineering (1)
- German PID-NET registry (1)
- HBT (1)
- HIV (1)
- Hadron production (1)
- Hadron-Hadron Scattering Heavy (1)
- Hadron-hadron interactions (1)
- Haemodialysis (1)
- Hard Scattering (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)
- High Energy Physics - Lattice (hep-lat) (1)
- High Energy Physics - Phenomenology (hep-ph) (1)
- High Energy Physics - Theory (hep-th) (1)
- Hyperons (1)
- IgG substitution therapy (1)
- Inclusive spectra (1)
- Intensity interferometry (1)
- Invariant Mass Distribution (1)
- Ionisation energy loss (1)
- Jet Physics (1)
- Jet Substructure (1)
- Job satisfaction (1)
- Lambda Calculus (1)
- Lebensqualität (1)
- Leukaemia (1)
- ML <Programmiersprache> (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)
- Musculoskeletal diseases (1)
- Muskuloskeletale Erkrankungen (1)
- NMDA IgA/IgM antibodies (1)
- NMDA antibody (1)
- Neural network (1)
- Nuclear Theory (nucl-th) (1)
- Nuclear modification factor (1)
- Nucleus (1)
- Occupational health (1)
- Office work (1)
- Operational Semantics (1)
- PID prevalence (1)
- PYTHIA (1)
- Parkinson disease (1)
- Particle and Resonance Production (1)
- Pb–Pb (1)
- Pedagogue (1)
- Pharmacodynamics (1)
- Production Cross Section (1)
- Properties of Hadrons (1)
- Proton (1)
- Proton–proton (1)
- Pädagoge/in (1)
- Quality of life (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)
- SF-36 (1)
- Single muons (1)
- Strangeness (1)
- Stretch training (1)
- Subjective health status (1)
- Subjektiver Gesundheitszustand (1)
- Systematic Uncertainty (1)
- TR (1)
- Tanz (1)
- Target validation (1)
- Time Projection Chamber (1)
- Tracking (1)
- Transition radiation detector (1)
- Transverse momentum (1)
- Treatment modification (1)
- Trigger (1)
- Vector Boson Production (1)
- Work health promotion (1)
- Xenon-based gas mixture (1)
- amplicon sequencing (1)
- anticoagulation (1)
- atrial fibrillation (1)
- bacteria (1)
- biogeographic legaciese (1)
- cART (1)
- dE/dx (1)
- decomposition (1)
- detector (1)
- experimental results (1)
- forest classification (1)
- forest functional similarity (1)
- heavy ion experiments (1)
- lambda calculus (1)
- left atrial appendage occlusion (1)
- metabarcoding (1)
- musculoskeletal disorders (1)
- nematode diversity (1)
- nondeterminism (1)
- occupational health (1)
- phylogenetic community distance (1)
- primary immunodeficiency (PID) (1)
- programming languages (1)
- quality of life (1)
- quark gluon plasma (1)
- registry for primary immunodeficiency (1)
- semantics (1)
- spectra (1)
- stretching (1)
- stroke (1)
- temperate forest (1)
- translation (1)
- trophic interactions (1)
- tropical forests (1)
- workplace health promotion (1)
- √sN N = 2.76 TeV (1)
Institute
- Physik (1052)
- Frankfurt Institute for Advanced Studies (FIAS) (958)
- Informatik (934)
- Medizin (18)
- Biochemie und Chemie (3)
- Informatik und Mathematik (3)
- ELEMENTS (2)
- Hochschulrechenzentrum (2)
- Biochemie, Chemie und Pharmazie (1)
- Biodiversität und Klima Forschungszentrum (BiK-F) (1)
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: Eukaryotic gene expression is controlled by cis-regulatory elements (CREs), including promoters and enhancers, which are bound by transcription factors (TFs). Differential expression of TFs and their binding affinity at putative CREs determine tissue- and developmental-specific transcriptional activity. Consolidating genomic data sets can offer further insights into the accessibility of CREs, TF activity, and, thus, gene regulation. However, the integration and analysis of multi-modal data sets are hampered by considerable technical challenges. While methods for highlighting differential TF activity from combined chromatin state data (e.g., ChIP-seq, ATAC-seq, or DNase-seq) and RNA-seq data exist, they do not offer convenient usability, have limited support for large-scale data processing, and provide only minimal functionality for visually interpreting results.
Results: We developed TF-Prioritizer, an automated pipeline that prioritizes condition-specific TFs from multi-modal data and generates an interactive web report. We demonstrated its potential by identifying known TFs along with their target genes, as well as previously unreported TFs active in lactating mouse mammary glands. Additionally, we studied a variety of ENCODE data sets for cell lines K562 and MCF-7, including twelve histone modification ChIP-seq as well as ATAC-seq and DNase-seq datasets, where we observe and discuss assay-specific differences.
Conclusion: TF-Prioritizer accepts ATAC-seq, DNase-seq, or ChIP-seq and RNA-seq data as input and identifies TFs with differential activity, thus offering an understanding of genome-wide gene regulation, potential pathogenesis, and therapeutic targets in biomedical research.
Background Eukaryotic gene expression is controlled by cis-regulatory elements (CREs) including promoters and enhancers which are bound by transcription factors (TFs). Differential expression of TFs and their putative binding sites on CREs cause tissue and developmental-specific transcriptional activity. Consolidating genomic data sets can offer further insights into the accessibility of CREs, TF activity, and thus gene regulation. However, the integration and analysis of multi-modal data sets are hampered by considerable technical challenges. While methods for highlighting differential TF activity from combined ChIP-seq and RNA-seq data exist, they do not offer good usability, have limited support for large-scale data processing, and provide only minimal functionality for visual result interpretation.
Results We developed TF-Prioritizer, an automated java pipeline to prioritize condition-specific TFs derived from multi-modal data. TF-Prioritizer creates an interactive, feature-rich, and user-friendly web report of its results. To showcase the potential of TF-Prioritizer, we identified known active TFs (e.g., Stat5, Elf5, Nfib, Esr1), their target genes (e.g., milk proteins and cell-cycle genes), and newly classified lactating mammary gland TFs (e.g., Creb1, Arnt).
Conclusion TF-Prioritizer accepts ChIP-seq and RNA-seq data, as input and suggests TFs with differential activity, thus offering an understanding of genome-wide gene regulation, potential pathogenesis, and therapeutic targets in biomedical research.
In vivo inducible reverse genetics in patients' tumors to identify individual therapeutic targets
(2021)
High-throughput sequencing describes multiple alterations in individual tumors, but their functional relevance is often unclear. Clinic-close, individualized molecular model systems are required for functional validation and to identify therapeutic targets of high significance for each patient. Here, we establish a Cre-ERT2-loxP (causes recombination, estrogen receptor mutant T2, locus of X-over P1) based inducible RNAi- (ribonucleic acid interference) mediated gene silencing system in patient-derived xenograft (PDX) models of acute leukemias in vivo. Mimicking anti-cancer therapy in patients, gene inhibition is initiated in mice harboring orthotopic tumors. In fluorochrome guided, competitive in vivo trials, silencing of the apoptosis regulator MCL1 (myeloid cell leukemia sequence 1) correlates to pharmacological MCL1 inhibition in patients´ tumors, demonstrating the ability of the method to detect therapeutic vulnerabilities. The technique identifies a major tumor-maintaining potency of the MLL-AF4 (mixed lineage leukemia, ALL1-fused gene from chromosome 4) fusion, restricted to samples carrying the translocation. DUX4 (double homeobox 4) plays an essential role in patients’ leukemias carrying the recently described DUX4-IGH (immunoglobulin heavy chain) translocation, while the downstream mediator DDIT4L (DNA-damage-inducible transcript 4 like) is identified as therapeutic vulnerability. By individualizing functional genomics in established tumors in vivo, our technique decisively complements the value chain of precision oncology. Being broadly applicable to tumors of all kinds, it will considerably reinforce personalizing anti-cancer treatment in the future.