We consider the two-dimensional Widom-Rowlinson lattice model. This discrete spin model describes a surface on Which a one to one mixture of two gases is sprayed.

These gases shall be strongly repelling on short distances.

We indicate the amount of gas by a positive parameter, the so called activity.

The main result of this thesis states that given an activity larger than 2, there are at most two ergodic Widom-Rowlinson measures if the underlying graph is the star lattice.

This falls naturally into two parts:

The first part is quite general and establishes a new sufficient condition for the existence of at most two ergodic Widom-Rowlinson measures.

This condition demands the existence of 1*lassos, i.e., 1*circuits 1*connected to the boundary, with probability bounded away from zero.

Our approach is based upon the infinite cluster method.

More precisely, we prevent the (co)existence of infinite clusters of certain types.

To this end, we first have to improve the existing results in this direction, which will be done in a general setting for two-dimensional dependent percolation.

The second part is devoted to verify the sufficient condition of the first part for activities larger than 2.

To this end, we have to compare the probabilities of configurations exhibiting 1*lassos to the ones exhibiting 0lassos.

This will be done by constructing an injection that fills certain parts of 0circuits with 1spins and, hereby, forms a 1*lasso.

Over the last decades collaborative learning has gained immensely in importance and popularity due to its high potential. Unfortunately, learners rarely engage in effective learning activities unless they are provided with instructional support. In order to maximize learning outcomes it is therefore advisable to structure collaborative learning sessions. One way of doing this is using collaboration scripts, which define a sequence of activities to be carried out by the learners. The field of computer-supported collaborative learning (CSCL) produced a variety of collaboration scripts that proved to have positive effects on learning outcomes. These scripts provide detailed descriptions of successful learning scenarios and are therefore used as foundation for this thesis.

In many cases computers are used to support collaborative learning. Traditional personal computers are often chosen for this purpose. However, during the last decades new technologies have emerged, which seem to be better suited for co-located collaboration than personal computers. Large interactive displays, for example, allow a number of people to work simultaneously on the same surface while being highly aware of the co-learners' actions. There are also multi-display environments that provide several workspaces, some of which may be shared, others may be personal. However, there is a lack of knowledge regarding the influence of different display types on group processes. For instance, it remains unclear in which cases shareable user interfaces should replace traditional single-user devices and when both personal and shared workspaces should be provided. This dissertation therefore explores the role of personal and shared workspaces in various situations in the area of collaborative learning. The research questions include the choice of technological devices, the seating arrangement as well as how user interfaces can be designed to guide learners.

To investigate these questions a two-fold approach was chosen. First, a framework was developed, which supports the implementation of scripted collaborative learning applications. Second, different prototypes were implemented to explore the research questions. Each prototype is based on at least one collaboration script. The result is a set of studies, which contribute to answering the above-mentioned research questions. With regard to the choice of display environment the studies showed several reasons for integrating personal devices such as laptops. Pure tabletop applications with around-the-table seating arrangements whose benefits for collaboration are widely discussed in the relevant literature revealed severe drawbacks for text-based learning activities. The combination of laptops and an interactive wall display, on the other hand, turned out to be a suitable display environment for collaborative learning in several cases. In addition, the thesis presents several ways of designing the user interface in a way that guides learners through collaboration scripts.

We give a new set theoretic system of axioms motivated by a topological intuition: The set of subsets of any set is a topology on that set. On the one hand, this system is a common weakening of Zermelo-Fraenkel set theory ZF, the positive set theory GPK and the theory of hyperuniverses. On the other hand, it retains most of the expressiveness of these theories and has the same consistency strength as ZF. We single out the additional axiom of the universal set as the one that increases the consistency strength to that of GPK and explore several other axioms and interrelations between those theories.

Hyperuniverses are a natural class of models for theories with a universal set. The Aleph_0- and Aleph_1-dimensional Cantor cubes are examples of hyperuniverses with additivity Aleph_0, because they are homeomorphic to their hyperspace. We prove that in the realm of spaces with uncountable additivity, none of the generalized Cantor cubes has that property.

Finally, we give two complementary constructions of hyperuniverses which generalize many of the constructions found in the literature and produce initial and terminal hyperuniverses.

With the growing amount of data handled by Internet-enabled

mobile devices, the task of preventing software from leaking

confidential information is becoming increasingly important. At

the same time, mobile applications are typically executed on

different devices whose users have varying requirements for the

privacy of their data. Users should be able to define their

personal information security settings, and they should get a

reliable assurance that the installed software respects these

settings. Language-based information flow security focuses on

the analysis of programs to determine information flows among

accessed data resources of different security levels, and to

verify and formally certify that these flows follow a given

policy. In the mobile code scenario, however, both the dynamic

aspect of the security environment and the fact that mobile

software is distributed as bytecode pose a challenge for existing

static analysis approaches. This thesis presents a

language-based mechanism to certify information flow security in

the presence of dynamic environments. An object-oriented

high-level language as well as a bytecode language are equipped

with facilities to inspect user-defined information flow security

settings at runtime. This way, the software developer can create

privacy-aware programs that can adapt their behaviour to

arbitrary security environments, a property that is formalized as

"universal noninterference". This property is statically

verified by an information flow type system that uses restrictive

forms of dependent types to judge abstractly on the concrete

security policy that is effective at runtime. To verify compiled

bytecode programs, a low-level version of the type system is

presented that works on an intermediate code representation in

which the original program structure is partially restored.

Rigorous soundness proofs and a type-preserving compilation

enable the generation of certified bytecode programs in the style

of proof-carrying code. To show the practical feasibility of the

approach, the system is implemented and demonstrated on a

concrete application scenario, where personal data are sent from

a mobile device to a server on the Internet.

The present thesis compares two computational interpretations of non-constructive proofs: refined A-translation and Gödel's functional "Dialectica" interpretation. The behaviour of the extraction methods is evaluated in the light of several case studies, where the resulting programs are analysed and compared. It is argued that the two interpretations correspond to specific backtracking implementations and that programs obtained via the refined A-translation tend to be simpler, faster and more readable than programs obtained via Gödel's interpretation.

Three layers of optimisation are suggested in order to produce faster and more readable programs. First, it is shown that syntactic repetition of subterms can be reduced by using let-constructions instead of meta substitutions abd thus obtaining a near linear size bound of extracted terms. The second improvement allows declaring syntactically computational parts of the proof as irrelevant and that this can be used to remove redundant parameters, possibly improving the efficiency of the program. Finally, a special case of induction is identified, for which a more efficient recursive extracted term can be defined. It is shown the outcome of case distinctions can be memoised, which can result in exponential improvement of the average time complexity of the extracted program.

In biological research, diverse high-throughput techniques enable the investigation of whole systems at the molecular level. The development of new methods and algorithms is necessary to analyze and interpret measurements of gene and protein expression and of interactions between genes and proteins. One of the challenges is the integrated analysis of gene expression and the associated regulation mechanisms.

The two most important types of regulators, transcription factors (TFs) and microRNAs (miRNAs), often cooperate in complex networks at the transcriptional and post-transcriptional level and, thus, enable a combinatorial and highly complex regulation of cellular processes. For instance, TFs activate and inhibit the expression of other genes including other TFs whereas miRNAs can post-transcriptionally induce the degradation of transcribed RNA and impair the translation of mRNA into proteins.

The identification of gene regulatory networks (GRNs) is mandatory in order to understand the underlying control mechanisms. The expression of regulators is itself regulated, i.e. activating or inhibiting regulators in varying conditions and perturbations. Thus, measurements of gene expression following targeted perturbations (knockouts or overexpressions) of these regulators are of particular importance. The prediction of the activity states of the regulators and the prediction of the target genes are first important steps towards the construction of GRNs.

This thesis deals with these first bioinformatics steps to construct GRNs. Targets of TFs and miRNAs are determined as comprehensively and accurately as possible. The activity state of regulators is predicted for specific high-throughput data and specific contexts using appropriate statistical approaches. Moreover, (parts of) GRNs are inferred, which lead to explanations of given measurements. The thesis describes new approaches for these tasks together with accompanying evaluations and validations. This immediately defines the three main goals of the current thesis:

1. The development of a comprehensive database of regulator-target relation.

Regulators and targets are retrieved from public repositories, extracted from the literature via text mining and collected into the miRSel database. In addition, relations can be predicted using various published methods. In order to determine the activity states of regulators (see 2.) and to infer GRNs (3.) comprehensive and accurate regulator-target relations are required.

It could be shown that text mining enables the reliable extraction of miRNA, gene, and protein names as well as their relations from scientific free texts. Overall, the miRSel contains about three times more relations for the model organisms human, mouse, and rat as compared to state-of-the-art databases (e.g. TarBase, one of the currently most used resources for miRNA-target relations).

2. The prediction of activity states of regulators based on improved target sets.

In order to investigate mechanisms of gene regulation, the experimental contexts have to be determined in which the respective regulators become active. A regulator is predicted as active based on appropriate statistical tests applied to the expression values of its set of target genes. For this task various gene set enrichment (GSE) methods have been proposed. Unfortunately, before an actual experiment it is unknown which genes are affected. The missing standard-of-truth so far has prevented the systematic assessment and evaluation of GSE tests. In contrast, the trigger of gene expression changes is of course known for experiments where a particular regulator has been directly perturbed (i.e. by knockout, transfection, or overexpression). Based on such datasets, we have systematically evaluated 12 current GSE tests. In our analysis ANOVA and the Wilcoxon test performed best.

3. The prediction of regulation cascades.

Using gene expression measurements and given regulator-target relations (e.g. from the m

Biological studies across all omics fields generate vast amounts of data. To understand these complex data, biologically motivated data mining techniques are indispensable. Evaluation of the high-throughput measurements usually relies on the identification of underlying signals as well as shared or outstanding characteristics. Therein, methods have been developed to recover source signals of present datasets, reveal objects which are more similar to each other than to other objects as well as to detect observations which are in contrast to the background dataset. Biological problems got individually addressed by using solutions from computer science according to their needs. The study of protein-protein interactions (interactome) focuses on the identification of clusters, the sub-graphs of graphs: A parameter-free graph clustering algorithm was developed, which was based on the concept of graph compression, in order to find sets of highly interlinked proteins sharing similar characteristics. The study of lipids (lipidome) calls for co-regulation analyses: To reveal those lipids similarly responding to biological factors, partial correlations were generated with differential Gaussian Graphical Models while accounting for solely disease-specific correlations. The study on single cell level (cytomics) aims to understand cellular systems often with the help of microscopy techniques: A novel noise robust source separation technique allowed to reliably extract independent components from microscopy images describing protein behaviors. The study of peptides (peptidomics) often requires the detection outstanding observations: By assessing regularities in the data set, an outlier detection algorithm was implemented based on compression efficacy of independent components of the dataset. All developed algorithms had to fulfill most diverse constraints in each omics field, but were met with methods derived from standard correlation and dependency analyses.