Refine
Year of publication
- 2012 (1235) (remove)
Document Type
- Article (575)
- Conference Proceeding (164)
- Part of Periodical (157)
- Book (131)
- Doctoral Thesis (79)
- Working Paper (53)
- Report (32)
- Part of a Book (26)
- Review (8)
- Preprint (4)
Language
- English (1235) (remove)
Keywords
- Pasolini, Pier Paolo (15)
- new species (13)
- taxonomy (11)
- Cape Verde Islands (8)
- Democracy (8)
- Koreanisch (8)
- Ellipse <Linguistik> (6)
- Law (6)
- apoptosis (6)
- human rights (6)
Institute
- Medizin (220)
- Rechtswissenschaft (103)
- Physik (99)
- Biowissenschaften (72)
- Biochemie und Chemie (70)
- Frankfurt Institute for Advanced Studies (FIAS) (54)
- Wirtschaftswissenschaften (45)
- Center for Financial Studies (CFS) (40)
- Informatik (40)
- Extern (31)
The diagram-based method to prove correctness of program transformations consists of computing
complete set of (forking and commuting) diagrams, acting on sequences of standard reductions
and program transformations. In many cases, the only missing step for proving correctness of a
program transformation is to show the termination of the rearrangement of the sequences. Therefore
we encode complete sets of diagrams as term rewriting systems and use an automated tool
to show termination, which provides a further step in the automation of the inductive step in
correctness proofs.
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a big-step semantics.
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.
Molecular biology of hearing
(2012)
The inner ear is our most sensitive sensory organ and can be subdivided into three functional units: organ of Corti, stria vascularis and spiral ganglion. The appropriate stimulus for the organ of hearing is sound, which travels through the external auditory canal to the middle ear where it is transmitted to the inner ear. The inner ear houses the hair cells, the sensory cells of hearing. The inner hair cells are capable of mechanotransduction, the transformation of mechanical force into an electrical signal, which is the basic principle of hearing. The stria vascularis generates the endocochlear potential and maintains the ionic homeostasis of the endolymph. The dendrites of the spiral ganglion form synaptic contacts with the hair cells. The spiral ganglion is composed of neurons that transmit the electrical signals from the cochlea to the central nervous system. In recent years there has been significant progress in research on the molecular basis of hearing. An increasing number of genes and proteins related to hearing are being identified and characterized. The growing knowledge of these genes contributes not only to greater appreciation of the mechanism of hearing but also to a deeper understanding of the molecular basis of hereditary hearing loss. This basic research is a prerequisite for the development of molecular diagnostics and novel therapies for hearing loss.
wo assumptions underlie current models of the geographical ranges of perennial plant species: 1. current ranges are in equilibrium with the prevailing climate, and 2. changes are attributable to changes in macroclimatic factors, including tolerance of winter cold, the duration of the growing season, and water stress during the growing season, rather than to biotic interactions. These assumptions allow model parameters to be estimated from current species ranges. Deterioration of growing conditions due to climate change, e.g. more severe drought, will cause local extinction. However, for many plant species, the predicted climate change of higher minimum temperatures and longer growing seasons means, improved growing conditions. Biogeographical models may under some circumstances predict that a species will become locally extinct, despite improved growing conditions, because they are based on an assumption of equilibrium and this forces the species range to match the species-specific macroclimatic thresholds. We argue that such model predictions should be rejected unless there is evidence either that competition influences the position of the range margins or that a certain physiological mechanism associated with the apparent improvement in growing conditions negatively affects the species performance. We illustrate how a process-based vegetation model can be used to ascertain whether such a physiological cause exists. To avoid potential modelling errors of this type, we propose a method that constrains the scenario predictions of the envelope models by changing the geographical distribution of the dominant plant functional type. Consistent modelling results are very important for evaluating how changes in species areas affect local functional trait diversity and hence ecosystem functioning and resilience, and for inferring the implications for conservation management in the face of climate change.
Power and law in enlightened absolutism : Carl Gottlieb Svarez' theoretical and practical approach
(2012)
The term Enlightened Absolutism reflects a certain tension between its two components. This tension is in a way a continuation of the dichotomy between power on one hand and law on the other. The present paper shall provide an analysis of these two concepts from the perspective of Carl Gottlieb Svarez, who, in his position as a high-ranking Prussian civil servant and legal reformist, has had unparalleled influence on the legislative history of the
Prussian states towards the end of the 18th century. Working side-by-side with Johann Heinrich Casimir von Carmer, who held the post of Prussian minister of justice from 1779 to 1798, Svarez was able to make use of his talent for reforming and legislating. From 1780 to 1794 he was primarily responsible for the elaboration of the codification of the Prussian private law – the “Allgemeines Landrecht für die Preußischen Staaten” in 1794. In the present paper, Svarez’ approach to the relation between law and power shall be analysed on two different levels. Firstly, on a theoretical level, the reformist’s thoughts and reflections as laid down in his numerous works, papers and memorandums, shall be discussed. Secondly, on a practical level, the question of the extent to which he implemented his ideas in Prussian legal reality shall be explored.
Background: Despite limited effectiveness of short-term psychotherapy for chronic depression, there is a lack of trials of long-term psychotherapy. Our study is the first to determine the effectiveness of controlled long-term psychodynamic and cognitive-behavioral (CBT) treatments and to assess the effects of preferential vs. randomized assessment.
Methods/design: Patients are assigned to treatment according to their preference or randomized (if they have no clear preference). Up to 80 sessions of psychodynamic or psychoanalytically oriented treatments (PAT) or up to 60 sessions of CBT are offered during the first year in the study. After the first year, PAT can be continued according to the ‘naturalistic’ usual method of treating such patients within the system of German health care (normally from 240 up to 300 sessions over two to three years). CBT therapists may extend their treatment up to 80 sessions, but focus mainly maintenance and relapse prevention. We plan to recruit a total of 240 patients (60 per arm). A total of 11 assessments are conducted throughout treatment and up to three years after initiation of treatment. The primary outcome measures are the Quick Inventory of Depressive Symptoms (QIDS, independent clinician rating) and the Beck Depression Inventory (BDI) after the first year.
Discussion: We combine a naturalistic approach with randomized controlled trials(RCTs)to investigate how effectively chronic depression can be treated on an outpatient basis by the two forms of treatment reimbursed in the German healthcare system and we will determine the effects of treatment preference vs. randomization.
This dissertation is concerned with the role of prosody and, specifically, linguistic rhythm for the syntactic processing of written text. My aim is to put forward, provide evidence for, and defend the following claims:
1. While processing written sentences, readers make use of their phonological knowledge and generate a mental prosodic-phonological representation of the printed text.
2. The mental prosodic representation is constructed in accordance with a syntactic description of the written string. Constraints at the interface of syntax and phonology provide for the compatibility of the syntactic analysis and the (mental) prosodic rendition of the sentence.
3. The implicit prosodic structure readers impose on the written string entails phonological phrasing and accentuation, but also lower level prosodic features such as linguistic rhythm which emerges from the pattern of stressed and unstressed syllables.
4. Phonological well-formedness conditions accompany and influence the process of syntactic parsing in reading from the very beginning, i.e. already at the level of recognizing lexical categories. At points of underspecified syntactic structure, syntactic parsing decisions may be made on the basis of phonological constraints alone.
5. In reading, the implicit local lexical-prosodic information may be more readily available to the processing mechanism than higher-level discourse structural representations and consequently may have more immediate influence on sentence processing.
6. The process of sentence comprehension in reading is conditioned by factors that are geared towards sentence production.
7. The interplay of syntactic and phonological processes in reading can be explained with recourse to a performance-compatible competence grammar.
The evidence from three reading experiments supports these points and suggests a model of grammatical competence in which constraints from various domains (syntax, semantics, pragmatics, discourse structure, and phonology) interact in providing the possible structural, i.e. grammatical descriptions.
Staphylococcus aureus proteins Sbi and Efb recruit human plasmin to degrade complement C3 and C3b
(2012)
Upon host infection, the human pathogenic microbe Staphylococcus aureus (S. aureus) immediately faces innate immune reactions such as the activated complement system. Here, a novel innate immune evasion strategy of S. aureus is described. The staphylococcal proteins surface immunoglobulin-binding protein (Sbi) and extracellular fibrinogen-binding protein (Efb) bind C3/C3b simultaneously with plasminogen. Bound plasminogen is converted by bacterial activator staphylokinase or by host-specific urokinase-type plasminogen activator to plasmin, which in turn leads to degradation of complement C3 and C3b. Efb and to a lesser extend Sbi enhance plasmin cleavage of C3/C3b, an effect which is explained by a conformational change in C3/C3b induced by Sbi and Efb. Furthermore, bound plasmin also degrades C3a, which exerts anaphylatoxic and antimicrobial activities. Thus, S. aureus Sbi and Efb comprise platforms to recruit plasmin(ogen) together with C3 and its activation product C3b for efficient degradation of these complement components in the local microbial environment and to protect S. aureus from host innate immune reactions.
Editorial
01 Foreword
Research & Policy
01 WP 12/06: Central Banks - Paradise Lost
02 Staff Member Profile
Events
01 The ECB and Its Watchers XIV
02 Greece: Getting Here and Moving Forward
03 Beyond Our Means: Why America Spends While the World Saves 04 How can Macro-Prudential Regulation be Effective?
05 Globalization and Pluralization of States. Why there will be no “United States of Europe”
06 Deutsche Bank Prize in Financial Economics 2013: Preview
Last but not least
01 Christian Leuz will visit Frankfurt with Humboldt Research Award
02 LOEWE center "Sustainable Architecture for Finance in Europe"
03 New Senior Fellows at CFS