962 Works

Machine-learning approaches for the empirical Schrödinger bridge problem

Francisco Vargas
The Schrödinger bridge problem is concerned with finding the most likely stochastic evolution between two probability distributions given a prior/reference stochastic evolution. This problem was posed by Schrödinger (1931, 1932) and solved to a large extent. Problems of this kind, whilst not popular in the machine learning community, have direct applications such as domain adaptation, hypothesis testing, semantic similarity, and others. Thus, the focus of this thesis is to carry out a preliminary study on...

On using Edinburgh LCF to prove the correctness of a parsing algorithm

Avra Cohn & Robin Milner
The methodology of Edinburgh LCF, a mechanized interactive proof system is illustrated through a problem suggested by Gloess – the proof of a simple parsing algorithm. The paper is self-contained, giving only the relevant details of the LCF proof system. It is shown how tactics may be composed in LCF to yield a strategy which is appropriate for the parser problem but which is also of a generally useful form. Also illustrated is a general...

Automatic mesh generation of 2 & 3 dimensional curvilinear manifolds

Burkard Wördenweber

Prediction oriented description of database systems

Mark Theodore Pezarro

An operational semantics for occam

Juanito Camilleri
Occam is a programming language designed to support concurrent applications, especially those implemented on networks of communicating processors. The aim of this paper is to formulate the meaning of the language constructs of Occam by semantic definitions which are intended as a direct formalisation of the natural language descriptions usually found in programming language manuals [Inmos 5]. This is done by defining a syntax directed transition system where the transitions associated to a phrase are...

PFL+: A Kernal Scheme for Functions I/O

Andrew Gordon
In place of the common separation of functional I/O into continuation and stream based schemes, an alternative division between Data Driven and Strictness Driven mechanisms for I/O is proposed. The data driven mechanism determines I/O actions by the Weak Head Normal Form of programs, while strictness driven I/O is based on suspensions – I/O actions are triggered when demand arises for the value of a suspension during normal order reduction. The data driven and strictness...

Natural language interfaces to databases

Ann Copestake & Karen Spärck Jones
This paper reviews the state of the art in natural language access to databases. This has been a long-standing area of work in natural language processing. But though some commercial systems are now available, providing front ends has proved much harder than was expected, and the necessary limitations on front ends have to be recognised. The paper discusses the issues, both general to language and task-specific, involved in front end design, and the way these...

Specification of computer architectures:
a survey and annotated bibliography

Timothy E. Leonard
I first define computer architecture and architecture specification, explain how the conflict between clarity and ambiguity makes writing specifications difficult, and introduce and consider the advantages and problems of formal specifications. I then survey all the literature on architecture specification, and introduce the literature on technical writing and on formal specification in general. I close with an annotated bibliography.

Inference in a natural language front end for databases

Ann Copestake & Karen Spärck Jones
This report describes the implementation and initial testing of knowledge representation and inference capabilities within a modular database front end designed for transportability.

Site interconnection and the exchange architecture

David Lawrence Tennenhouse

Ordered rewriting and confluence

Ursula Martin & Tobias Nipkow

A verified compiler for a verified microprocessor

Jeffrey J. Joyce

A mechanised definition of Silage in HOL

Andrew D. Gordon
If formal methods of hardware verification are to have any impact on the practices of working engineers, connections must be made between the languages used in practice to design circuits, and those used for research into hardware verification. Silage is a simple dataflow language marketed for specifying digital signal processing circuits. Higher Order Logic (HOL) is extensively used for research into hardware verification. This paper presents a formal definition of a substantial subset of Silage,...

Functional programming and input/output

Andrew Donald Gordon

Efficiency in a fully-expansive theorem prover

Richard John Boulton
The HOL system is a fully-expansive theorem prover: Proofs generated in the system are composed of applications of the primitive inference rules of the underlying logic. This has two main advantages. First, the soundness of the system depends only on the implementations of the primitive rules. Second, users can be given the freedom to write their own proof procedures without the risk of making the system unsound. A full functional programming language is provided for...

An architecture for distributed user interfaces

Stephen Martin Guy Freeman
Computing systems have changed rapidly since the first graphical user interfaces were developed. Hardware has become faster and software architectures have become more flexible and more open; a modern computing system consists of many communicating machines rather than a central host. Understanding of human-computer interaction has also become more sophisticated and places new demands on interactive software; these include, in particular, support for multi-user applications, continuous media, and ‘ubiquitous’ computing. The layer which binds user...

A concrete final coalgebra theorem for ZF set theory

Lawrence C. Paulson
A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo-Fraenkel set theory. Aczel’s Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel’s Solution and Substitution Lemmas are proved in the style of Rutten and Turi (1993). The approach is less general than Aczel’s; non-well-founded objects can...

The contour tree image encoding technique and file format

Martin John Turner

Personal projected displays

Mark S. D. Ashdown
Since the inception of the personal computer, the interface presented to users has been defined by the monitor screen, keyboard, and mouse, and by the framework of the desktop metaphor. It is very different from a physical desktop which has a large horizontal surface, allows paper documents to be arranged, browsed, and annotated, and is controlled via continuous movements with both hands. The desktop metaphor will not scale to such a large display; the continuing...

Role-based access control policy administration

András Belokosztolszki
The wide proliferation of the Internet has set new requirements for access control policy specification. Due to the demand for ad-hoc cooperation between organisations, applications are no longer isolated from each other; consequently, access control policies face a large, heterogeneous, and dynamic environment. Policies, while maintaining their main functionality, go through many minor adaptations, evolving as the environment changes. In this thesis we investigate the long-term administration of role-based access control (RBAC) – in particular...

Compromising emanations: eavesdropping risks of computer displays

Markus G. Kuhn
Electronic equipment can emit unintentional signals from which eavesdroppers may reconstruct processed data at some distance. This has been a concern for military hardware for over half a century. The civilian computer-security community became aware of the risk through the work of van Eck in 1985. Military “Tempest” shielding test standards remain secret and no civilian equivalents are available at present. The topic is still largely neglected in security textbooks due to a lack of...

A role and context based security model

Yolanta Beresnevichiene
Security requirements approached at the enterprise level initiate the need for models that capture the organisational and distributed aspects of information usage. Such models have to express organisation-specific security policies and internal controls aiming to protect information against unauthorised access and modification, and against usage of information for unintended purposes. This technical report describes a systematic approach to modelling the security requirements from the perspective of job functions and tasks performed in an organisation. It...

Formal verification of probabilistic algorithms

Joe Hurd
This thesis shows how probabilistic algorithms can be formally verified using a mechanical theorem prover. We begin with an extensive foundational development of probability, creating a higher-order logic formalization of mathematical measure theory. This allows the definition of the probability space we use to model a random bit generator, which informally is a stream of coin-flips, or technically an infinite sequence of IID Bernoulli(1/2) random variables. Probabilistic programs are modelled using the state-transformer monad familiar...

Using inequalities as term ordering constraints

Joe Hurd
In this paper we show how linear inequalities can be used to approximate Knuth-Bendix term ordering constraints, and how term operations such as substitution can be carried out on systems of inequalities. Using this representation allows an off-the-shelf linear arithmetic decision procedure to check the satisfiability of a set of ordering constraints. We present a formal description of a resolution calculus where systems of inequalities are used to constrain clauses, and implement this using the...

Emotion inference from human body motion

Daniel Bernhardt
The human body has evolved to perform sophisticated tasks from locomotion to the use of tools. At the same time our body movements can carry information indicative of our intentions, inter-personal attitudes and emotional states. Because our body is specialised to perform a variety of everyday tasks, in most situations emotional effects are only visible through subtle changes in the qualities of movements and actions. This dissertation focuses on the automatic analysis of emotional effects...

Registration Year

  • 2022
  • 2021

Resource Types

  • Report