Now showing items 215-234 of 380

    • A Machine-Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets 

      Paulson, Lawrence Charles (Cambridge University Press, 2014-04-03)
      A formalization of Gödel’s incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows ...
    • Managing Privacy, Rights, and Security in a Digital Economy 

      Angelopoulos, Spyros; Mortier, Richard Michael; mcauley, derek; Merali, Y; price, dominic
      We focus on the issues of managing Big Data within a Digital Economy, and address the asymmetrical distribution of power between the originators of data and the organizations that make use of that data. We propose a framework ...
    • Mathematical Information Retrieval based on type embeddings and query expansion 

      Stathopoulos, YA; Teufel, Simone Heidi (International Committee on Computational Linguistics, 2016-12)
      We present an approach to mathematical information retrieval (MIR) that exploits a special kind of technical terminology, referred to as a mathematical type. In this paper, we present and evaluate a type detection mechanism ...
    • Measuring similarity between gene expression profiles: a Bayesian approach 

      Unknown author (2009-12-03)
      Abstract Background Grouping genes into clusters on the basis of similarity between their expression profiles has been the main approach to predict functional modules, from which important inference or further investigation ...
    • Measuring Urban Social Diversity Using Interconnected Geo-Social Networks 

      Hristova, Desislava; Williams, Matthew J; Musolesi, Mirco; Panzarasa, Pietro; Mascolo, Cecilia (Association for Computing Machinery, 2016-04-16)
      Large metropolitan cities bring together diverse individuals, creating opportunities for cultural and intellectual exchanges, which can ultimately lead to social and economic enrichment. In this work, we present a novel ...
    • A Mechanised Proof of Gödel’s Incompleteness Theorems using Nominal Isabelle 

      Paulson, Lawrence Charles (Springer, 2015-05-02)
      An Isabelle/HOL formalisation of Gödel’s two incompleteness theorems is presented. The work follows Swierczkowski’s detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical ...
    • Mechanising and Verifying the WebAssembly Specification 

      Watt, Conrad
      WebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as ...
    • Mechanizing coinduction and corecursion in higher-order logic 

      Paulson, Lawrence Charles (1997-01-01)
    • Mind the Gap: A Comparison of Software Packet Generators 

      Emmerich, P; Gallenmüller, S; Antichi, Gianni; Moore, Andrew William; Carle, G (IEEE, 2017-05-18)
      Network research relies on packet generators to assess performance and correctness of new ideas. Software-based generators in particular are widely used by academic researchers because of their flexibility, affordability, ...
    • Minimizing Detection Probability Routing in Ad Hoc Networks Using Directional Antennas 

      Unknown author (2009-06-08)
      In a hostile environment, it is important for a transmitter to make its wireless transmission invisible to adversaries because an adversary can detect the transmitter if the received power at its antennas is strong enough. ...
    • Mining Open Datasets for Transparency in Taxi Transport in Metropolitan Environments 

      Noulas, Anastasios; Salnikov, Vsevolod; Lambiotte, Renaud; Mascolo, Cecilia (Springer, 2015-12-10)
      Uber has recently been introducing novel practices in urban taxi transport. Journey prices can change dynamically in almost real time and also vary geographically from one area to another in a city, a strategy known as ...
    • Mining Users' Significant Driving Routes with Low-power Sensors 

      Nawaz, Sarfraz; Mascolo, Cecilia (ACM, 2014)
      While there is significant work on sensing and recognition of significant places for users, little attention has been given to users’ significant routes. Recognizing these routine journeys, opens doors to the development ...
    • The Missing Link: Explaining ELF Static Linking, Semantically 

      Kell, Stephen; Mulligan, Dominic Phillip; Sewell, Peter Michael (Association for Computing Machinery, 2016-10-19)
      Beneath the surface, software usually depends on com- plex linker behaviour to work as intended. Even linking hello_world.c is surprisingly involved, and systems software such as libc and operating system kernels rely on ...
    • Misuse of information and communications technology within the public sector 

      Hutchings, Alice; Jorna, Penny (Australian Institute of Criminology, 2015)
      Misuse of information and communications technology (ICT) includes theft of hardware and software, unauthorised access to computer systems and inappropriate use of equipment. Internal unauthorised access is recognised as ...
    • Mixed-size concurrency: ARM, POWER, C/C++11, and SC 

      Flur, Shaked; Sarkar, Susmit; Pulte, Christopher; Nienhuis, Kyndylan; Maranget, L; Gray, Kathryn Elizabeth; Sezgin, Ali et al. (Association for Computing Machinery, 2017-01-01)
      Previous work on the semantics of relaxed shared-memory concurrency has only considered the case in which each load reads the data of exactly one store. In practice, however, multiprocessors support mixed-size accesses, ...
    • Mobile Sensing at the Service of Mental Well-being: a Large-scale Longitudinal Study 

      Servia-Rodríguez, S; Rachuri, KK; Mascolo, Cecilia; Rentfrow, Peter Jason; Lathia, N; Sandstrom, GM
      Measuring mental well-being with mobile sensing has been an increasingly active research topic. Pervasiveness of smartphones combined with the convenience of mobile app distribution platforms (e.g., Google Play) provide a ...
    • Modal Kleene Algebra Applied to Program Correctness 

      Gomes, Victor; Struth, Georg (Springer, 2016)
      Modal Kleene algebras are relatives of dynamic logics that support program construction and verification by equational reasoning. We describe their application in implementing versatile program correctness components in ...
    • A model of local adaptation 

      Vangorp, P; Myszkowski, K; Graf, EW; Mantiuk, Rafal Konrad (ACM, 2015-11-01)
      The visual system constantly adapts to different luminance levels when viewing natural scenes. The state of visual adaptation is the key parameter in many visual models. While the time-course of such adaptation is well ...
    • A model of register transfer systems with applications to microcode and VLSI correctness 

      Gordon, Michael John (Department of Computer Science, University of Edinburgh, 1982-05)
      In this paper we describe and illustrate a simple semantic model of register transfer systems — i.e. systems built by connecting together storage devices like registers and.memories via combinational circuits like gates ...