1,161 Works

Automatic summarising of English texts

John Irving Tait
This thesis describes a computer program called Scrabble which can summarise short English texts. It uses large bodies of predictions about the likely contents of texts about particular topics to identify the commonplace material in an input text. Pre-specified summary templates, each associated with a different topic are used to condense the commonplace material in the input. Filled-in summary templates are then used to form a framework into which unexpected material in the input may...

The design of a ring communication network

Steven Temple
This dissertation describes the design of a high speed local area network. Local networks have been in use now for over a decade and there is a proliferation of different systems, experimental ones which are not widely used and commercial ones installed in hundreds of locations. For a new network design to be of interest from the research point of view it must have a feature or features which set it apart from existing networks...

Using information systems to solve recursive domain equations effectively

Glynn Winskel & Kim Guldstrand Larsen
This paper aims to make two main contributions. One is to show how to use the concrete nature of Scott’s information systems to advantage in solving recursive domain equations. The method is based on the substructure relation between information systems. This essentially makes a complete partial order (cpo) of information systems. Standard domain constructions like function space can be made continuous on this cpo so the solution of recursive domain equations reduces to the more...

Intelligent network interfaces

Nicholas Henry Garnett

A new type-checker for a functional language

Jon Fairbairn
A polymorphic type checker for the functional language Ponder [Fairbairn 82] is described. The initial sections give an overview of the syntax of Ponder, and some of the motivation behind the design of the type system. This is followed by a definition of the relation of ‘generality’ between these types, and of the notion of type-validity of Ponder programs. An algorithm to determine whether a Ponder program is type-valid is then presented. The final sections...

Some notes on mass terms and plurals

Ann Copestake
This report describes a short investigation into some possible treatments of mass nouns and plurals. It aims to provide a grammar and axiomatisation with a reasonable coverage of these phenomena, so that a range of sentences can be parsed, and inferences made automatically. The previous work on the subject, mainly due to Hasle (1988) is reviewed, and the limitations of both the original theories and Hasle’s implementation are demonstrated. Some more recent work, especially that...

Evaluation Logic

Andrew M. Pitts
A new typed, higher-order logic is described which appears particularly well fitted to reasoning about forms of computation whose operational behaviour can be specified using the Natural Semantics style of structural operational semantics. The logic’s underlying type system is Moggi’s computational metalanguage, which enforces a distinction between computations and values via the categorical structure of a strong monad. This is extended to a (constructive) predicate logic with modal formulas about evaluation of computations to values,...

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...

The semantics and implementation of aggregates
how to express concurrency without destroying determinism

Thomas Clarke
This paper investigates the relationship between declarative semantics and concurrent computation. A fundamental programming construction, the aggregate, is identified. Aggregates have a simple declarative semantics, yet cannot be written in pure functional languages. The addition of aggregates to a functional language increases expressiveness without destroying determinism or referential transparency. Specific aggregates can be used to implememnt concurrent graph marking, time deterministic merge of lazy lists, and write once locations.

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.

Higher-order critical pairs

Tobias Nipkow
We consider rewrite systems over simply typed λ-terms with restricted left-hand sides. This gives rise to a one-step reduction relation whose transitive, reflexive and symmetric closure coincides with equality. The main result of this paper is a decidable confluence criterion which extends the well-known critical pairs to a higher-order setting. Several applications to typed λ-calculi and proof theory are shown.

Site interconnection and the exchange architecture

David Lawrence Tennenhouse

Formal verification of VIPER’s ALU

Wai Wong

Categorical abstract machines for higher-order typed lambda calculi

Eike Ritter

Storage and presentation support for multimedia applications in a distributed, ATM network environment

Jean Bacon, John Bates, Sai Lai Lo & Ken Moody
We are building a display platform for multimedia applications above a multi-service storage architecture (MSSA). This style of application needs high speed ATM networks and suitable protocols and operating systems; an infrastructure that exists at the University of Cambridge Computer Laboratory. An open storage architecture gives flexibility and extensibility. Conventional files, audio, video and structured objects are supported within a common architectural framework and composite objects, such as a display representation, may have components of...

Set theory for verification: II
Induction and recursion

Lawrence C. Paulson
A theory of recursive definitions has been mechanized in Isabelle’s Zermelo-Fraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other computational reasoning. Inductively defined sets are expressed as least fixedpoints, applying the Knaster-Tarski Theorem over a suitable set. Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the Knaster-Tarski Theorem...

Co-induction and co-recursion in higher-order logic

Lawrence C. Paulson
A theory of recursive and corecursive definitions has been developed in higher-order logic (HOL) and mechanised using Isabelle. Least fixedpoints express inductive data types such as strict lists; greatest fixedpoints express co-inductive data types, such as lazy lists. Well-founded recursion expresses recursive functions over inductive data types; co-recursion expresses functions that yield elements of co-inductive data types. The theory rests on a traditional formalization of infinite trees. The theory is intended for use in specification...

Proof by pointing

Yves Bertot, Gilles Kahn & Laurent Théry

A verified Vista implementation

Paul Curzon

A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia

Jacques Fleuriot & Lawrence C. Paulson
The theorem prover Isabelle is used to formalise and reproduce some of the styles of reasoning used by Newton in his Principia. The Principia’s reasoning is resolutely geometric in nature but contains “infinitesimal” elements and the presence of motion that take it beyond the traditional boundaries of Euclidean Geometry. These present difficulties that prevent Newton’s proofs from being mechanised using only the existing geometry theorem proving (GTP) techniques. Using concepts from Robinson’s Nonstandard Analysis (NSA)...

Video mail retrieval using voice
Report on topic spotting

G.J.F. Jones, J.T. Foote, K. Sparck Jones & S.J. Young

Symbol grounding:
Learning categorical and sensorimotor predictions for coordination in autonomous robots

Karl F. MacDorman

Global/local subtyping for a distributed π-calculus

Peter Sewell
In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type system for a distributed π-calculus in which the input and output of channels may be either global or local. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. Recursive types and products are...

Minimizing latency of agreement protocols

Piotr Zieliński
Maintaining consistency of fault-tolerant distributed systems is notoriously difficult to achieve. It often requires non-trivial agreement abstractions, such as Consensus, Atomic Broadcast, or Atomic Commitment. This thesis investigates implementations of such abstractions in the asynchronous model, extended with unreliable failure detectors or eventual synchrony. The main objective is to develop protocols that minimize the number of communication steps required in failure-free scenarios but remain correct if failures occur. For several agreement problems and their numerous...

Cassandra: flexible trust management and its application to electronic health records

Moritz Y. Becker
The emergence of distributed applications operating on large-scale, heterogeneous and decentralised networks poses new and challenging problems of concern to society as a whole, in particular for data security, privacy and confidentiality. Trust management and authorisation policy languages have been proposed to address access control and authorisation in this context. Still, many key problems have remained unsolved. Existing systems are often not expressive enough, or are so expressive that access control becomes undecidable; their semantics...

Registration Year

  • 2021
  • 2020
  • 2019
  • 2018
  • 2017
  • 2016
  • 2015

Resource Types

  • Report


  • Bonn-Rhein-Sieg University of Applied Sciences
  • Lyrasis
  • University of Strathclyde
  • King's College London
  • Swinburne University of Technology
  • University of Sydney
  • Plymouth University
  • University of Gothenburg
  • University of Leoben
  • University of Massachusetts Boston