Bøker i Distinguished Dissertations in Computer Science-serien

Computing systems are becoming highly complex, harder to understand, and therefore more prone to failure. It is important therefore that we are able to employ mathematical techniques to specify the behaviour of critical safety systems. The research contained in this book represents work on the specification and verification of real-time systems.

We are surrounded by noise; to separate the signals we want to hear from those we do not we have developed various strategies. Giving computers similar abilities would help develop devices such as intelligent hearing aids. This book reviews new and recent work on the modelling of auditory processes.

There are essentially two radically different approaches to robot navigation: the first uses a map of the robot's environment; the second requires the robot to react rapidly to local sensory information. This book is the first to give a practical method for evaluating the different approaches to determine the best exploration strategy.

The author provides a homogeneous treatment of the semantics of both theoretical and practical logic programming languages. Researchers interested in logic programming or semantics, as well as artificial intelligence search strategies need to consult this book as the only source for some essential and new ideas in the area.

The first book presenting a stochastic extension of process algebra; this can be applied to performance modelling. The method, which is illustrated with case studies taken from the area of communication systems, can readily be used to construct a variety of models that can be analysed using standard numerical techniques.

This book describes the use of qualified types to provide a general framework for the combination of polymorphism and overloading, concentrating in particular on the implementation of overloading in Haskell and Gofer.

Computer vision is a rapidly growing field which aims to make computers 'see' as effectively as humans. In this book, based on his award-winning thesis, Dr Shapiro presents a new computer vision framework for interpreting time-varying imagery.

First published in 1991, this thesis concentrates upon the design of three-dimensional, rather than the traditional two-dimensional, circuits. The theory behind such circuits is presented in detail, together with experimental results.

First published in 1993, this thesis is concerned with the design of efficient algorithms for listing combinatorial structures. Some related work is also included which compares the listing problem with the difficulty of solving the existence problem, the construction problem, the random sampling problem, and the counting problem.

In this 1995 book Dr Lo, winner of a Distinguished Dissertation Award, defined a multi-service storage architecture that could meet the needs of existing and emerging applications and support multiple file abstractions. He also explored a number of related design issues.

Axiomatic categorical domain theory is crucial for understanding the meaning of programs and reasoning about them. This book is the first systematic account of the subject and studies mathematical structures suitable for modelling functional programming languages in an axiomatic (i.e. abstract) setting. In particular, the author develops theories of partiality and recursive types and applies them to the study of the metalanguage FPC; for example, enriched categorical models of the FPC are defined. Furthermore, FPC is considered as a programming language with a call-by-value operational semantics and a denotational semantics defined on top of a categorical model. To conclude, for an axiomatisation of absolute non-trivial domain-theoretic models of FPC, operational and denotational semantics are related by means of computational soundness and adequacy results. To make the book reasonably self-contained, the author includes an introduction to enriched category theory.