This thesis provides a computational interpretation of type theory validating Brouwer’s uniform-continuity principle that all functions from the Cantor space to natural numbers are uniformly continuous, so that type-theoretic proofs with the principle as an assumption have computational content. For this, we develop a variation of Johnstone’s topological topos, which consists of sheaves on a certain uniform-continuity site that is suitable for predicative, constructive reasoning. Our concrete sheaves can be described as sets equipped with a suitable continuity structure, which we call C-spaces, and their natural transformations can be regarded as continuous maps. The Kleene-Kreisel continuous functional can be calculated within the category of C-spaces. Our C-spaces form a locally cartesian closed category with a natural numbers object, and hence give models of Gödel’s system T and of dependent type theory. Moreover, the category has a fan functional that continuously compute moduli of uniform continuity, which validates the uniform-continuity principle formulated as a skolemized formula in system T and as a type via the Curry-Howard interpretation in dependent type theory. We emphasize that the construction of C-spaces and the verification of the uniform-continuity principles have been formalized in intensional Martin-Löf type theory in Agda notation.

Automated reasoning technology provides means for inference in a formal context via a multitude of disparate reasoning techniques. Combining different techniques not only increases the effectiveness of single systems but also provides a more powerful approach to solving hard problems. Consequently combined reasoning systems have been successfully employed to solve non-trivial mathematical problems in combinatorially rich domains that are intractable by traditional mathematical means. Nevertheless, the lack of domain specific knowledge often limits the effectiveness of these systems. In this thesis we investigate how the combination of diverse reasoning techniques can be employed to pre-compute additional knowledge to enable mathematical discovery in finite and potentially infinite domains that is otherwise not feasible. In particular, we demonstrate how we can exploit bespoke symbolic computations and automated theorem proving to automatically compute and evolve the structural knowledge of small size finite structures in the algebraic theory of quasigroups. This allows us to increase the solvability horizon of model generation systems to find solution models for large size finite algebraic structures previously unattainable. We also present an approach to exploring infinite models using a mixture of automated tools and user interaction to iteratively inspect the structure of solutions and refine search. A practical implementation combines a specialist term rewriting system with bespoke graph algorithms and visualization tools and has been applied to solve the generalized version of Kuratowski's classical closure-complement problem from point-set topology that had remained open for several years.

Research in Virtual Heritage has gained popularity in recent years. Efforts by the community of Virtual Heritage researchers to reconstruct sites considered worthy of preservation span from the historical “built environment”, including the Pyramids at Ghiza and Virtual Reality Notre Dame, to natural heritage sites such as Australia’s Great Barrier Reef and the Virtual Everglades at Florida. Other important efforts to conserve artefacts and educate visitors include Virtual Stonehenge, Pompeii and the Caves of Lascaux. Entire villages, cities and even caves have been constructed as part of virtual conservation efforts. These digital reconstructions have, to date, contributed significant awareness and interest among the general public, providing educational benefits to schoolchildren and new research opportunities to archaeologists and conservationists, to mention but two groups of beneficiaries. Today, to paraphrase the work of Professor Robert J. Stone, Virtual Heritage strives to deliver to a global audience, computer-based reconstructions of artefacts, sites and actors of historic, artistic, religious and cultural heritage in such a way as to provide formative educational experience through the manipulations of time and space. It is realised that the user experience and educational value of a Virtual Heritage site is crucial – the process of virtual reconstruction is as important as its outcome. The total experience therefore, hinges on the modelling accuracy, scientific credibility, and the interactive visualisation capability of a virtual site. However, many interactive media implementations in Virtual Heritage in the recent past have failed to make full use of the advanced interactive visualisation techniques available to researchers. In particular, an element that many end users might consider essential, namely the inclusion of “living” and responsive virtual agents are noticeably lacking in most all Virtual Heritage examples. The addition of these ‘living’ entities and environments could give Virtual Heritage applications a richer, more evolvable content, and a higher level of interactivity. Artificial Life (alife), an emerging research area dealing with the study of synthetic systems that exhibit behaviours characteristic of natural living systems, offers great potential in overcoming this missing element in current Virtual Heritage applications. The present research investigates the feasibility of constructing models of vegetation, exploiting new developments in Artificial Life implemented within a controlled Virtual Environment for application in the field of Archaeology. The specific area of study is the recently discovered and recently named Shotton river valley off the eastern coast of the United Kingdom – a region that once flourished during the Mesolithic Era prior to the post-glacial flooding of the North Sea.

Modern Internet services are increasingly leveraging on cloud computing for flexible, elastic and on-demand provision. Typically, Quality of Service (QoS) of cloud-based services can be tuned using different underlying cloud configurations and resources, e.g., number of threads, CPU and memory etc., which are shared, leased and priced as utilities. This benefit is fundamentally grounded by autoscaling: an automatic and elastic process that adapts cloud configurations on-demand according to time-varying workloads. This thesis proposes a holistic cloud autoscaling framework to effectively and seamlessly address existing challenges related to different logical aspects of autoscaling, including architecting autoscaling system, modelling the QoS of cloudbased service, determining the granularity of control and deciding trade-off autoscaling decisions. The framework takes advantages of the principles of self-awareness and the related algorithms to adaptively handle the dynamics, uncertainties, QoS interference and trade-offs on objectives that are exhibited in the cloud. The major benefit is that, by leveraging the framework, cloud autoscaling can be effectively achieved without heavy human analysis and design time knowledge. Through conducting various experiments using RUBiS benchmark and realistic workload on real cloud setting, this thesis evaluates the effectiveness of the framework based on various quality indicators and compared with other state-of-the-art approaches.

In the last decade digital devices and services have permeated many aspects of everyday life. They generate massive amounts of data that provide insightful information about how people move across geographic areas and how they interact with others. By analysing this detailed information, it is possible to investigate aspects of human mobility and interaction. Therefore, the thesis of this dissertation is that the analysis of mobility and interaction traces generated by digital devices and services, at different timescales and spatial granularity, can be used to gain a better understanding of human behaviour, build new applications and improve existing services. In order to substantiate this statement I develop analytical models and applications supported by three sources of mobility and interaction data: online social networks, mobile phone networks and GPS traces. First, I present three applications related to data gathered from online social networks, namely the analysis of a global rumour spreading in Twitter, the definition of spatial dissemination measures in a social graph and the analysis of collaboration between developers in GitHub. Then I describe two applications of the analysis of country-wide data of cellular phone networks: the modelling of epidemic containment strategies, with the goal of assessing their efficacy in curbing infectious diseases; the definition of a mobility-based measure of individual risk, which can be used to identify who needs targeted treatment. Finally, I present two applications based on GPS traces: the estimation of trajectories from spatially-coarse temporally-sparse location traces and the analysis of routing behaviour in urban settings.

This thesis proposes the engineering of an elastic self-adaptive security solution for the Cloud that considers assets as independent entities, with a need for customised, ad-hoc security. The solution exploits agent-based, market-inspired methodologies and learning approaches for managing the changing security requirements of assets by considering the shared and on-demand nature of services and resources while catering for monetary and computational constraints. The usage of auction procedures allows the proposed framework to deal with the scale of the problem and the trade-offs that can arise between users and Cloud service provider(s). Whereas, the usage of a learning technique enables our framework to operate in a proactive, automated fashion and to arrive on more efficient bidding plans, informed by historical data. A variant of the proposed framework, grounded on a simulated university application environment, was developed to evaluate the applicability and effectiveness of this solution. As the proposed solution is grounded on market methods, this thesis is also concerned with asserting the dependability of market mechanisms. We follow an experimentally driven approach to demonstrate the deficiency of existing market-oriented solutions in facing common market-specific security threats and provide candidate, lightweight defensive mechanisms for securing them against these attacks.

Planning under uncertainty is a common requirement of robot navigation. Probabilistic roadmaps are an efficient method for generating motion graphs through the robot's configuration space, but do not inherently represent any uncertainty in the environment. In this thesis, the physical domain is abstracted into a graph search problem where the states of some edges are unknown. This is modelled as a decision-theoretic planning problem described through a partially observable Markov Decision Process (POMDP). It is shown that the optimal policy can depend on accounting for the value of information from observations. The model scalability and the graph size that can be handled is then extended by conversion to a belief state Markov Decision Process. Approximations to both the model and the planning algorithm are demonstrated that further extend the scalability of the techniques for static graphs. Experiments conducted verify the viability of these approximations by producing near-optimal plans in greatly reduced time compared to recent POMDP solvers. Belief state approximation in the planner reduces planning time significantly while producing plans of equal quality to those without this approximation. This is shown to be superior to other techniques such as heuristic weighting which is not found to give any significant benefit to the planner.

Practical computers have only finite amounts of memory. However, the programs that run on them are often written in languages that effectively assume (via providing constructs such as general recursion) that infinite memory is available, meaning that an implementation of those programs is necessarily an approximation. The main focus of this thesis is on the use of contraction: the ability to use a function parameter more than once in the body of that function (or more generally, to mention a free variable more than once in a term). Unrestricted contraction is a common reason for a language to require unbounded amounts of memory to implement. This thesis looks at a range of type systems, both existing and new, that restrict the use of contraction so that they can be implemented with finite amounts of state, identifying common themes, and explaining and suggesting solutions for common deficiencies. In particular, different restrictions on contraction are seen to correspond to different features of the language’s implementation.

Evolution is notorious for its creative power, but also for giving rise to complex, unpredictable dynamics. As a result, practitioners of artificial evolution have encountered difficulties in predicting, analysing, or even understanding the outcome of their experiments. In particular, the concept of evolutionary "progress" (whether in the sense of performance increase or complexity growth) has given rise to much debate and confusion. After a careful description of the mechanisms of evolution and natural selection, we provide usable concepts of performance and progress in coevolution. In particular, we introduce a distinction between three types of progress: local, historical, and global, which we suggest underlies much of the confusion that surrounds coevolutionary dynamics. Similarly, we provide a comprehensive answer to the question of whether an "arrow of complexity" exists in evolution. We introduce several methods to detect and analyse performance and progress in coevolutionary experiments. We propose a statistical measure (Fitness Transmission) to detect the presence of adaptive Darwinian evolution in a reproducing population, based solely on genealogic records; we also point out the limitations of a popular method (the Bedau-Packard statistics of evolutionary activity) for this purpose. To test and illustrate our results, we implement a rich experimental system, inspired by the seminal work of Karl Sims, in which virtual creatures can evolve and interact under various conditions in a physically realistic three-dimensional (3D) environment. To our knowledge, this is the first complete reimplementation and extension of Sims' results. We later extend this system with the introduction of physical combat between creatures, also a first. Finally, we introduce Evosphere, an open, planet-like environment in which 3D artificial creatures interact, reproduce and evolve freely. We conclude our discussion by using Fitness Transmission to detect the onset of adaptive evolution in this system.

We investigate partial functions and computability theory from within a constructive, univalent type theory. The focus is on placing computability into a larger mathematical context, rather than on a complete development of computability theory. We begin with a treatment of partial functions, using the notion of dominance, which is used in synthetic domain theory to discuss classes of partial maps. We relate this and other ideas from synthetic domain theory to other approaches to partiality in type theory. We show that the notion of dominance is difficult to apply in our setting: the set of �0 1 propositions investigated by Rosolini form a dominance precisely if a weak, but nevertheless unprovable, choice principle holds. To get around this problem, we suggest an alternative notion of partial function we call disciplined maps. In the presence of countable choice, this notion coincides with Rosolini’s. Using a general notion of partial function,we take the first steps in constructive computability theory. We do this both with computability as structure, where we have direct access to programs; and with computability as property, where we must work in a program-invariant way. We demonstrate the difference between these two approaches by showing how these approaches relate to facts about computability theory arising from topos-theoretic and typetheoretic concerns. Finally, we tie the two threads together: assuming countable choice and that all total functions N - N are computable (both of which hold in the effective topos), the Rosolini partial functions, the disciplined maps, and the computable partial functions all coincide. We observe, however, that the class of all partial functions includes non-computable partial functions.