[Abridged abstract] The goal is to give structural proof-theoretical analyses of logical constants, and thereby provide a criterion for what a logical constant is. Another goal is to illustrate the thesis that structural assumptions of logic are basic and that alternative logics (later called substructural logics) differ from each other only in their structural assumptions, and not in their assumptions about logical constants.

This thesis is concerned with a conjecture of Zilber: that the complex field expanded with the exponential function should be `quasi-minimal'; that is, all its definable subsets should be countable or have countable complement. Our purpose is to study the geometry of this structure and other expansions by holomorphic functions of the complex field without having first to settle any number-theoretic problems, by treating all countable sets on an equal footing. We present axioms, modelled on those for a Zariski geometry, defining a non-first-order class of ``quasi-Zariski'' structures endowed with a dimension theory and a topology in which all countable sets are of dimension zero. We derive a quantifier elimination theorem, implying that members of the class are quasi-minimal. We look for analytic structures in this class. To an expansion of the complex field by entire holomorphic functions $\mathcal{R}$ we associate a sheaf $\mathcal{O}^{\scriptscriptstyle{\mathcal{R}}}$ of analytic germs which is closed under application of the implicit function theorem. We prove that $\mathcal{O}^{\scriptscriptstyle{\mathcal{R}}}$ is also closed under partial differentiation and that it admits Weierstrass preparation. The sheaf defines a subclass of the analytic sets which we call $\mathcal{R}$-analytic. We develop analytic geometry for this class proving a Nullstellensatz and other classical properties. We isolate a condition on the asymptotes of the varieties of certain functions in $\mathcal{R}$. If this condition is satisfied then the $\mathcal{R}$-analytic sets induce a quasi-Zariski structure under countable union. In the motivating case of the complex exponential we prove a low-dimensional case of the condition, towards the original conjecture.

The thesis deals with definability of certain Zariski geometries, introduced by Zilber, in the theory of algebraically closed fields. I axiomatise a class of structures, called 'abstract linear spaces', which are a common reduct of these Zariski geometries. I then describe what an interpretation of an abstract linear space in an algebraically closed field looks like. I give a new proof that the structure "quantum harmonic oscillator", introduced by Zilber and Solanki, is not interpretable in an algebraically closed field. I prove that a similar structure from an unpublished note of Solanki is not definable in an algebraically closed field and explain the non-definability of both structures in terms of geometric interpretation of the group law on a Galois cohomology group H¹(k(x), μ_n). I further consider quantum Zariski geometries introduced by Zilber and give necessary and sufficient conditions that a quantum Zariski geometry be definable in an algebraically closed field. Finally, I take an attempt at extending the results described above to complex-analytic setting. I define what it means for quantum Zariski geometry to have a complex analytic model, an give a necessary and sufficient conditions for a smooth quantum Zariski geometry to have one. I then prove a theorem giving a partial description of an interpretation of an abstract linear space in the structure of compact complex spaces and discuss the difficulties that present themselves when one tries to understand interpretations of abstract linear spaces and quantum Zariski geometries in the compact complex spaces structure.

In this thesis we present a framework for automatic formal analysis of competitive stochastic systems, such as sensor networks, decentralised resource management schemes or distributed user-centric environments. We model such systems as stochastic multi-player games, which are turn-based models where an action in each state is chosen by one of the players or according to a probability distribution. The specifications, such as “sensors 1 and 2 can collaborate to detect the target with probability 1, no matter what other sensors in the network do” or “the controller can ensure that the energy used is less than 75 mJ, and the algorithm terminates with probability at least 0.5'', are provided as temporal logic formulae. We introduce a branching-time temporal logic rPATL and its multi-objective extension to specify such probabilistic and reward-based properties of stochastic multi-player games. We also provide algorithms for these logics that can either verify such properties against the model, providing a yes/no answer, or perform strategy synthesis by constructing the strategy for the players that satisfies the specification. We conduct a detailed complexity analysis of the model checking problem for rPATL and its multi-objective extension and provide efficient algorithms for verification and strategy synthesis. We also implement the proposed techniques in the PRISM-games tool and apply them to the analysis of several case studies of competitive stochastic systems.

I explore five topics in topology using set-theoretic techniques. The first of these is a generalization of 2-point sets called slice sets. I show that, for any small-in-cardinality subset A of the real line, there is a subset of the plane meeting every line in a topological copy of A. Under Martin's Axiom, I show how to improve this result to any totally disconnected A. Secondly, I show that it is consistent with and independent of ZFC to have a topologically rigid subset of the real line that is smaller than the continuum. Thirdly, I define and examine a new cardinal function related to cleavability. Fourthly, I explore the Toronto Problem and prove that any uncountable, Hausdorff, non-discrete Toronto space that is not regular falls into one of two strictly-defined classes. I also prove that for every infinite cardinality there are precisely 3 non-T1 Toronto spaces up to homeomorphism. Lastly, I examine a notion of dimension called the "neight", and prove several theorems that give a lower bound for this cardinal function.

Hoare and He's Unifying Theories of Programming (UTP) provides a rich model of programs as relational predicates. This theory is intended to provide a single framework in which any programming paradigms, languages, and features, can be modelled, compared and contrasted. The UTP already has models for several programming formalisms, such as imperative programming, higher-order programming (e.g. programing with procedures), several styles of concurrent programming (or reactive systems), class-based object-orientation, and transaction processing. We believe that the UTP ought to be able to represent all significant computer programming language formalisms, in order for it to be considered a unifying theory. One gap in the UTP work is that of object-based object-orientation, such as that presented in Abadi and Cardelli's untyped object calculi (sigma-calculi). These sigma-calculi provide a prominent formalism of object-based object-oriented (OO) programs, which models programs as objects. We address this gap within this dissertation by presenting an embedding of an Abadi--Cardelli-style object calculus in the UTP. More formally, the thesis that his dissertation argues is that it is possible to provide an object-based object rientation to the UTP, with value- and reference-based objects, and a fully abstract model of references. We have made three contributions to our area of study: first, to extend the UTP with a notion of object-based object orientation, in contrast with the existing class-based models; second, to provide an alternative model of pointers (references) for the UTP that supports both value-based compound values (e.g. objects) and references (pointers), in contrast to existing UTP models with pointers that have reference-based compound values; and third, to model an Abadi-Cardelli notion of an object in the UTP, and thus demonstrate that it can unify this style of object formalism.

This thesis studies the categorical formalisation of quantum computing, through the prism of type theory, in a three-tier process. The first stage of our investigation involves the creation of the dagger lambda calculus, a lambda calculus for dagger compact categories. Our second contribution lifts the expressive power of the dagger lambda calculus, to that of a quantum programming language, by adding classical control in the form of complementary classical structures and dualisers. Finally, our third contribution demonstrates how our lambda calculus can be applied to various well known problems in quantum computation: Quantum Key Distribution, the quantum Fourier transform, and the teleportation protocol.

Alternating timed automata are a powerful extension of classical Alur-Dill timed automata that are closed under all Boolean operations. They have played a key role, among others, in providing verification algorithms for prominent specification formalisms such as Metric Temporal Logic. Unfortunately, when interpreted over an infinite dense time domain (such as the reals), alternating timed automata have an undecidable language emptiness problem. In this thesis we consider restrictions on this model that restore the decidability of the language emptiness problem. We consider the restricted class of safety alternating timed automata, which can encode a corresponding Safety fragment of Metric Temporal Logic. This thesis connects these two formalisms with insertion channel machines, a model of faulty communication, and demonstrates that the three formalisms are interreducible. We thus prove a non-elementary lower bound for the language emptiness problem for 1-clock safety alternating timed automata and further obtain a new proof of decidability for this problem. Complementing the restriction to safety properties, we consider interpreting the automata over bounded dense time domains. We prove that the time-bounded language emptiness problem is decidable but non-elementary for unrestricted alternating timed automata. The language emptiness problem for alternating timed automata is a special case of a much more general and abstract logical problem: Church's synthesis problem. Given a logical specification S(I,O), Church's problem is to determine whether there exists an operator F that implements the specification in the sense that S(I,F(I)) holds for all inputs I. It is a classical result that the synthesis problem is decidable in the case that the specification and implementation are given in monadic second-order logic over the naturals. We prove that this decidability extends to MSO over the reals with order and furthermore to MSO over every fixed bounded interval of the reals with order and the +1 relation.

Model checking is an automatic formal verification technique for establishing correctness of systems. It has been widely used in industry for analysing and verifying complex safety-critical systems in application domains such as avionics, medicine and computer security, where manual testing is infeasible and even minor errors could have dire consequences. In our increasingly parallelised world, concurrency has become pivotal and seamlessly woven within programming paradigms, however, extremely challenging when it comes to modelling and establishing correctness of intended behaviour. Tools for model checking concurrent systems face severe limitations due to scalability problems arising from the need to examine all possible interleavings (schedules) of executions of parallel components. Moreover, concurrency poses additional challenges to model checking, giving rise to phenomena such as nondeterminism, deadlock, livelock, etc. In this thesis we focus on adapting and developing novel model-checking techniques for concurrent systems in the setting of the process algebra CSP and its primary model checker FDR. CSP allows for a compact modelling and precise analysis of event-based concurrency, grounded on synchronous message passing as a fundamental mechanism of inter-component communication. In particular, we investigate techniques based on symbolic model checking, static analysis and abstraction, all of them exploiting the compositionality inherent in CSP and targeting to increase the scale of systems that can be tractably analysed. Firstly, we investigate symbolic model-checking techniques based on Boolean satisfiability (SAT), which we adapt for the traces model of CSP. We tailor bounded model checking (BMC), that can be used for bug detection, and temporal k-induction, which aims at establishing inductiveness of properties and is capable of both bug finding and establishing the correctness of systems. Secondly, we propose a static analysis framework for establishing livelock freedom of CSP processes, with lessons for other concurrent formalisms. As opposed to traditional exhaustive state-space exploration, our framework employs a system of rules on the syntax of a process to calculate a sound approximation of its fair/co-fair sets of events. The rules either safely classify a process as livelock-free or report inconclusiveness, thereby trading accuracy for speed. Finally, we develop a series of abstraction/refinement schemes for the traces, stable-failures and failures-divergences models of CSP and embed them into a fully automated and compositional CEGAR framework. For each of those techniques we present an implementation and an experimental evaluation on a set of CSP benchmarks.

This thesis is concerned with aspects of the model theory of infinite soluble groups. The results proved lie on the border between group theory and model theory: the questions asked are of a model-theoretic nature but the techniques used are mainly group-theoretic in character. We present a characterization of those groups contained in the universal closure of a restricted wreath product U wr G, where U is an abelian group of zero or finite square-free exponent and G is a torsion-free soluble group with a bound on the class of its nilpotent subgroups. For certain choices of G we are able to use this characterization to prove further results about these groups; in particular, results related to the decidability of their universal theories. The latter part of this work consists of a number of independent but related topics. We show that if G is a finitely generated abelian-by-metanilpotent group and H is elementarily equivalent to G then the subgroups gamma_n(G) and gamma_n(H) are elementarily equivalent, as are the quotient groups G/gamma_n(G) and G/gamma_n(H). We go on to consider those groups universally equivalent to F_2(VN_c), where the free groups of the variety V are residually finite p-groups for infinitely many primes p, distinguishing between the cases when c = 1 and when c > 2. Finally, we address some important questions concerning the theories of free groups in product varieties V_k · · ·V_1, where V_i is a nilpotent variety whose free groups are torsion-free; in particular we address questions about the decidability of the elementary and universal theories of such groups. Results mentioned in both of the previous two paragraphs have applications here.