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.

<p>This sentence is whatever truth is <em>not</em>. The subject of this master’s thesis is the power, influence, and solvability of the liar paradox. This paradox can be constructed through the application of a standard conception of truth and rules of inference are applied to sentences such as the first sentence of this abstract. The liar has been a powerful problem of philosophy for thousands of years, from its ancient origin (examined in Chapter One) to a particularly intensive period in the twentieth century featuring many ingenious but ultimately unsuccessful solutions from brilliant logicians, mathematicians and philosophers (examined in Chapter Two, Chapter Three, and Chapter Four). Most of these solutions were unsuccessful because of a recurring problem known as the liar’s revenge; whatever truth is <em>not</em> includes, as it turns out, not <em>just</em> falsity, but also meaninglessness, ungroundedness, gappyness, and so on. The aim of this master’s thesis is to prove that we should not consign ourselves to the admission that the liar is and always will just be a paradox, and thus unsolvable. Rather, I argue that the liar <em>is</em> solvable; I propose and defend a novel solution which is examined in detail in the latter half of Chapter Two, and throughout Chapter Three. The alternative solution I examine and endorse (in Chapter Four) is not my own, owing its origin and energetic support to Graham Priest. I argue, however, for a more qualified version of Priest’s solution. I show that, even if we accept a very select few true contradictions, it should <em>not</em> be assumed that inconsistency inevitably spreads throughout other sets of sentences used to describe everyday phenomena such as motion, change, and vague predicates in the empirical world.</p> / Master of Arts (MA)

<p>The main subject of investigation is the so-called "immediate expansion''<br />phenomenon in various first-order valued-field structures over the<br />corresponding underlying field structures. In particular, certain "valued<br />o-minimal fields'', certain Henselian valued fields with non-divisible valued<br />groups, and certain separably closed valued fields of finite imperfection degree, are<br />shown to have this property.</p> / Doctor of Philosophy (PhD)

The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories. String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string graphs has provided a combinatorial formalisation of string diagrams, laying the foundations for this project. The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning. This dissertation firstly extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation – and structures to encode it – to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. This can be used to represent, for example, the "spider law" of CFAs, allowing two spiders to be merged, as well as the much more complex generalised bialgebra law that can arise from two interacting CFAs. This work then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.

A philosophic account of quantum physics. The thesis is divided into two parts. Part I is dedicated to laying the groundwork of quantum physics, and explaining some of the primary difficulties. Subjects of interest will include the principle of locality, the quantum uncertainty principle, and Einstein's criterion for reality. Quantum dilemmas discussed include the double-slit experiment, observations of spin and polarization, EPR, and Bell's theorem. The first part will argue that mathematical-physical descriptions of the world fall short of explaining the experimental observations of quantum phenomenon. The problem, as will be argued, is framework of the physical descriptive schema. Part I includes in-depth discussions of mathematical principles. Part II will discuss the Copenhagen interpretation as put forth by its founders. The Copenhagen interpretation will be expressed as a paradox: The classical physical language cannot describe quantum phenomenon completely and with certainty, yet this language is the only possible method of articulating the physical world. The paradox of Copenhagen will segway into Kant's critique of metaphysics. Kant's understanding of causality, things-in-themselves, and a priori synthetic metaphysics. The thesis will end with a conclusion of the quantum paradox by juxtaposing anti-materialist Martin Heidegger with quantum founder Werner Heisenberg. Our conclusion will be primarily a discussion of how we understand the world, and specifically how our understanding of the world creates potential for truth.