The JACKDAW database package Challis, M.F. University of Cambridge, Computer Laboratory 1974-10 en Text UCAM-CL-TR-1 ISSN 1476-2986 This report describes a general database package which has been implemented in BCPL on an IBM 370/165 at the University of Cambridge. One current application is the provision of an administrative database for the Computing Service. Entries within a database may include (in addition to primitive fields such as ‘salary’ and ‘address’) links to other entries: each link represents a relationship between two entries and is always two-way. Generality is achieved by including within each database class definitions which define the structure of the entries within it; these definitions may be interrogated by program. The major part of the package presents a procedural interface between an application program and an existing database, enabling entries and their fields to be created, interrogated, updated and deleted. The creation of a new database (or modification of an existing one) by specifying the class definitions is handled by a separate program. The first part of the report describes the database structure and this is followed by an illustration of the procedural interface. Finally, some of the implementation techniques used to insure integrity of the database are described. Scheduling for a share of the machine Larmouth, J. University of Cambridge, Computer Laboratory 1974-10 en Text UCAM-CL-TR-2 ISSN 1476-2986 This paper describes the mechanism used to schedule jobs and control machine use on the IBM 370/165 at Cambridge University, England. The same algorithm is currently being used in part at the University of Bradford and implementations are in progress or under study for a number of other British Universities. The system provides computer management with a simple tool for controlling machine use. The managerial decision allocates a share of the total machine resources to each user of the system, either directly, or via a hierarchial allocation scheme. The system then undertakes to vary the turnaround of user jobs to ensure that those decisions are effective, no matter what sort of work the user is doing. At the user end of the system we have great flexibility in the way in which he uses the resources he has received, allowing him to get a rapid turnaround for those (large or small) jobs which require it, and a slower turnaround for other jobs. Provided he does not work at a rate exceeding that appropriate to his share of the machine, he can request, for every job he submits, the ‘deadline’ by which he wants it running, and the system will usually succeed in running his job at about the requested time – rarely later, and only occasionally sooner. Every job in the machine has its own ‘deadline’, and the machine is not underloaded. Within limits, each user can request his jobs back when he wants them, and the system keeps his use to within the share of the machine he has been given. The approach is believed to be an original one and to have a number of advantages over more conventional scheduling and controlling algorithms. A replacement for the OS/360 disc space management routines Stoneley, A.J.M. University of Cambridge, Computer Laboratory 1975-04 en Text UCAM-CL-TR-3 ISSN 1476-2986 In the interest of efficiency, the IBM disc space management routines (Dadsm) have been completely replaced in the Cambridge 370/165. A large reduction in the disc traffic has been achieved by keeping the lists of free tracks in a more compact form and by keeping lists of free VTOC blocks. The real time taken in a typical transaction has been reduced by a factor of twenty. By writing the code in a more appropriate form than the original, the size has been decreased by a factor of five, thus making it more reasonable to keep it permanently resident. The cpu requirement has decreased from 5% to 0.5% of the total time during normal service. The new system is very much safer than the old in the fact of total system crashes. The old system gave little attention to the consequences of being stopped in mid-flight, and it was common to discover an area of disc allocated to two files. This no longer happens. The dynamic creation of I/O paths under OS/360-MVT Stoneley, A.J.M. University of Cambridge, Computer Laboratory 1975-04 en Text UCAM-CL-TR-4 ISSN 1476-2986 In a large computer it is often desirable and convenient for an ordinary program to be able to establish for itself a logical connection to a peripheral device. This ability is normally provided through a routine within the operating system which may be called by any user program at any time. OS/360 lacks such a routine. For the batch job, peripheral connections can only be made through the job control language and this cannot be done dynamically at run-time. In the restricted context of TSO (IBM’s terminal system) a routine for establishing peripheral connections does exist, but it is extremely inefficient and difficult to use. This paper describes how a suitable routine was written and grafted into the operating system of the Cambridge 370/165. Parrot – A replacement for TCAM Hazel, P. Stoneley, A.J.M. University of Cambridge, Computer Laboratory 1976-04 en Text UCAM-CL-TR-5 ISSN 1476-2986 The terminal driving software and hardware for the Cambridge TSO (Phoenix) system is described. TCAM and the IBM communications controller were replaced by a locally written software system and a PDP-11 complex. This provided greater flexibility, reliability, efficiency and a better “end-user” interface than was possible under a standard IBM system. System programming in a high level language Birrell, Andrew D. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-6 ISSN 1476-2986 Local area computer communications network Hopper, Andrew University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-7 ISSN 1476-2986 Evaluation of a protection system Cook, Douglas John University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-9 ISSN 1476-2986 Prediction oriented description of database systems Pezarro, Mark Theodore University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-10 ISSN 1476-2986 Automatic resolution of linguistic ambiguities Boguraev, Branimir Konstatinov University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-11 ISSN 1476-2986 The thesis describes the design, implementation and testing of a natural language analysis system capable of performing the task of generating paraphrases in a highly ambiguous environment. The emphasis is on incorporating strong semantic judgement in an augmented transition network grammar: the system provides a framework for examining the relationship between syntax and semantics in the process of text analysis, especially while treating the related phenomena of lexical and structural ambiguity. Word-sense selection is based on global analysis of context within a semantically well-formed unit, with primary emphasis on the verb choice. In building structures representing text meaning, the analyser relies not on screening through many alternative structures – intermediate, syntactic or partial semantic – but on dynamically constructing only the valid ones. The two tasks of sense selection and structure building are procedurally linked by the application of semantic routines derived from Y. Wilks’ preference semantics, which are invoked at certain well chosen points of the syntactic constituent analysis – this delimits the scope of their action and provides context for a particular disambiguation technique. The hierarchical process of sentence analysis is reflected in the hierarchical organisation of application of these semantic routines – this allows the efficient coordination of various disambiguation techniques, and the reduction of syntactic backtracking, non-determinism in the grammar, and semantic parallelism. The final result of the analysis process is a dependency structure providing a meaning representation of the input text with labelled components centred on the main verb element, each characterised in terms of semantic primitives and expressing both the meaning of a constituent and its function in the overall textual unit. The representation serves as an input to the generator, organised around the same underlying principle as the analyser – the verb is central to the clause. Currently the generator works in paraphrase mode, but is specifically designed so that with minimum effort and virtually no change in the program control structure and code it could be switched over to perform translation. The thesis discusses the rationale for the approach adopted, comparing it with others, describes the system and its machine implementation, and presents experimental results. HASP “IBM 1130” multileaving remote job entry protocol with extensions as used on the University of Cambridge IBM 370/165 Oakley, M.R.A. Hazel, P. University of Cambridge, Computer Laboratory 1979-09 en Text UCAM-CL-TR-12 ISSN 1476-2986 Resource allocation and job scheduling Hazel, Philip University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-13 ISSN 1476-2986 The mechanisms for sharing the resources of the Cambridge IBM 370/165 computer system among many individual users are described. File store is treated separately from other resources such as central processor and channel time. In both cases, flexible systems that provide incentives to thrifty behaviour are used. The method of allocating resources directly to users rather than in a hierarchical manner via faculties and departments is described, and its social acceptability is discussed. Store to store swapping for TSO under OS/MVT Powers, J.S. University of Cambridge, Computer Laboratory 1980-06 en Text UCAM-CL-TR-14 ISSN 1476-2986 A system of store-to-store swapping incorporated into TSO on the Cambridge IBM 370/165 is described. Unoccupied store in the dynamic area is used as the first stage of a two-stage backing store for swapping time-sharing sessions; a fixed-head disc provides the second stage. The performance and costs of the system are evaluated. The implementation of BCPL on a Z80 based microcomputer Wilson, I.D. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-15 ISSN 1476-2986 The main aim of this project was to achieve as full an implementation as possible of BCPL on a floppy disc based microcomputer, running CP/M or CDOS (the two being esentially compatible). On the face of it there seemed so many limiting factors, that, when the project was started, it was not at all clear which one (if any) would become a final stumbling block. As it happened, the major problems that cropped up could be programmed round, or altered in such a way as to make them soluble. The main body of the work splits comfortably into three sections, and the writer hopes that, in covering each section separately, to be able to show how the whole project fits together into the finished implementation. Reliable storage in a local network Dion, Jeremy University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-16 ISSN 1476-2986 Three papers on parsing Boguraev, B.K. Spärck Jones, K. Tait, J.I. University of Cambridge, Computer Laboratory 1982 en Text UCAM-CL-TR-17 ISSN 1476-2986 Automatic mesh generation of 2 & 3 dimensional curvilinear manifolds Wördenweber, Burkard University of Cambridge, Computer Laboratory 1981-11 en Text UCAM-CL-TR-18 ISSN 1476-2986 Analysis and inference for English Cater, Arthur William Sebright University of Cambridge, Computer Laboratory 1981-09 en Text UCAM-CL-TR-19 ISSN 1476-2986 On using Edinburgh LCF to prove the correctness of a parsing algorithm Cohn, Avra Milner, Robin University of Cambridge, Computer Laboratory 1982-02 en Text UCAM-CL-TR-20 ISSN 1476-2986 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 mechanized method of deriving structural induction rules within the system. The correctness of a precedence parsing algorithm in LCF Cohn, A. University of Cambridge, Computer Laboratory 1982-04 en Text UCAM-CL-TR-21 ISSN 1476-2986 This paper describes the proof in the LCF system of a correctness property of a precedence parsing algorithm. The work is an extension of a simpler parser and proof by Cohn and Milner (Cohn & Milner 1982). Relevant aspects of the LCF system are presented as needed. In this paper, we emphasize (i) that although the current proof is much more complex than the earlier one, mqany of the same metalanguage strategies and aids developed for the first proof are used in this proof, and (ii) that (in both cases) a general strategy for doing some limited forward search is incorporated neatly into the overall goal-oriented proof framework. Constraints in CODD Robson, M. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-22 ISSN 1476-2986 The paper describes the implementation of the data structuring concepts of domains, intra-tuple constraints and referential constraints in the relational DBMS CODD. All of these constraints capture some of the semantics of the database’s application. Each class of constraint is described briefly and it is shown how each of them is specified. The constraints are stored in the database giving a centralised data model, which contains descriptions of procedures as well as of statistic structures. Some extensions to the notion of referential constraint are proposed and it is shown how generalisation hierarchies can be expressed as sets of referential constraints. It is shown how the stored data model is used in enforcement of the constraints. Two papers about the scrabble summarising system Tait, J.I. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-23 ISSN 1476-2986 This report contains two papers which describe parts of the Scrabble English summarizing system. The first, “Topic identification techniques for predictive language analyzers” has been accepted as a short communication for the 9th International COnference on Computational Linguistics, in Prague. The second, “General summaries using a predictive language analyser” is an extended version of a discussion paper which will be presented at the European Conference on Artificial Intelligence in Paris. Both conferences will take place during July 1982. The [second] paper describes a computer system capable of producing coherent summaries of English texts even when they contain sections which the system has not understood completely. The system employs an analysis phase which is not dissimilar to a script applier together with a rather more sophisticated summariser than previous systems. Some deficiencies of earlier systems are pointed out, and ways in which the current implementation overcomes them are discussed. Steps towards natural language to data language translation using general semantic information Boguraev, B.K. Spärck Jones, K. University of Cambridge, Computer Laboratory 1982-03 en Text UCAM-CL-TR-24 ISSN 1476-2986 A clustering technique for semantic network processing Alshawi, Hiyan University of Cambridge, Computer Laboratory 1982-05 en Text UCAM-CL-TR-25 ISSN 1476-2986 Portable system software for personal computers on a network Knight, Brian James University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-26 ISSN 1476-2986 Exception handling in domain based systems Johnson, Martyn Alan University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-27 ISSN 1476-2986 Poly report Matthews, D.C.J. University of Cambridge, Computer Laboratory 1982-08 en Text UCAM-CL-TR-28 ISSN 1476-2986 Poly was designed to provide a programming system with the same flexibility as a dynamically typed language but without the run-time oveheads. The type system, based on that of Russel allows polymorpphic operations to be used to manipulate abstract objects, but with all the type checking being done at compile-time. Types may be passed explicitly or by inference as parameters to procedures, and may be returned from procedures. Overloading of names and generic types can be simulated by using the general procedure mechanism. Despite the generality of the language, or perhaps because of it, the type system is very simple, consisting of only three classes of object. There is an exception mechanism, similar to that of CLU, and the exceptions raised in a procedure are considered as part of its ‘type’. The construction of abstract objects and hiding of internal details of the representation come naturally out of the type system. Introduction to Poly Matthews, D.C.J. University of Cambridge, Computer Laboratory 1982-05 en Text UCAM-CL-TR-29 ISSN 1476-2986 This report is a tutorial introduction to the programming language Poly. It describes how to write and run programs in Poly using the VAX/UNIX implementation. Examples given include polymorphic list functions, a double precision integer package and a subrange type constructor. A portable BCPL library Wilkes, John University of Cambridge, Computer Laboratory 1982-10 en Text UCAM-CL-TR-30 ISSN 1476-2986 Ponder and its type system Fairbairn, J. University of Cambridge, Computer Laboratory 1982-11 en Text UCAM-CL-TR-31 ISSN 1476-2986 This note describes the programming language “Ponder”, which is designed according to the principles of referencial transparency and “orthogonality” as in [vWijngaarden 75]. Ponder is designed to be simple, being functional with normal order semantics. It is intended for writing large programmes, and to be easily tailored to a particular application. It has a simple but powerful polymorphic type system. The main objective of this note is to describe the type system of Ponder. As with the whole of the language design, the smallest possible number of primitives is built in to the type system. Hence for example, unions and pairs are not built in, but can be constructed from other primitives. How to drive a database front end using general semantic information Boguraev, B.K. Spärck Jones, K. University of Cambridge, Computer Laboratory 1982-11 en Text UCAM-CL-TR-32 ISSN 1476-2986 An island parsing interpreter for Augmented Transition Networks Carroll, John A. University of Cambridge, Computer Laboratory 1982-10 en Text UCAM-CL-TR-33 ISSN 1476-2986 This paper describes the implementation of an ‘island parsing’ interpreter for an Augmented Transition Network (ATN). The interpreter provides more complete coverage of Woods’ original ATM formalism than his later island parsing implementation; it is written in LISP and has been modestly tested. Recent developments in LCF: examples of structural induction Paulson, Larry University of Cambridge, Computer Laboratory 1983-01 en Text UCAM-CL-TR-34 ISSN 1476-2986 Rewriting in Cambridge LCF Paulson, Larry University of Cambridge, Computer Laboratory 1983-02 en Text UCAM-CL-TR-35 ISSN 1476-2986 Many automatic theorem-provers rely on rewriting. Using theorems as rewrite rules helps to simplify the subgoals that arise during a proof. LCF is an interactive theorem-prover intended for reasoning about computation. Its implementation of rewriting is presented in detail. LCF provides a family of rewriting functions, and operators to combine them. A succession of functions is described, from pattern matching primitives to the rewriting tool that performs most inferences in LCF proofs. The design is highly modular. Each function performs a basic, specific task, such as recognizing a certain form of tautology. Each operator implements one method of building a rewriting function from simpler ones. These pieces can be put together in numerous ways, yielding a variety of rewriting strategies. The approach involves programming with higher-order functions. Rewriting functions are data values, produced by computation on other rewriting functions. The code is in daily use at Cambridge, demonstrating the practical use of functional programming. The revised logic PPLAMBDA : A reference manual Paulson, Lawrence University of Cambridge, Computer Laboratory 1983-03 en Text UCAM-CL-TR-36 ISSN 1476-2986 PPLAMBDA is the logic used in the Cambridge LCF proof assistant. It allows Natural Deduction proofs about computation, in Scott’s theory of partial orderings. The logic’s syntax, axioms, primitive inference rules, derived inference rules and standard lemmas are described as are the LCF functions for building and taking apart PPLAMBDA formulas. PPLAMBDA’s rule of fixed-point induction admits a wide class of inductions, particularly where flat or finite types are involved. The user can express and prove these type properties in PPLAMBDA. The induction rule accepts a list of theorems, stating type properties to consider when deciding to admit an induction. Representation and authentication on computer networks Girling, Christopher Gray University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-37 ISSN 1476-2986 Views and imprecise information in databases Gray, Mike University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-38 ISSN 1476-2986 Tactics and tacticals in Cambridge LCF Paulson, Lawrence University of Cambridge, Computer Laboratory 1983-07 en Text UCAM-CL-TR-39 ISSN 1476-2986 The SKIM microprogrammer’s guide Stoye, W. University of Cambridge, Computer Laboratory 1983-10 en Text UCAM-CL-TR-40 ISSN 1476-2986 LCF_LSM, A system for specifying and verifying hardware Gordon, Mike University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-41 ISSN 1476-2986 Proving a computer correct with the LCF_LSM hardware verification system Gordon, Mike University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-42 ISSN 1476-2986 Extending the local area network Leslie, Ian Malcom University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-43 ISSN 1476-2986 This dissertation is concerned with the development of a large computer network which has many properties associated with local area computer networks, including high bandwidth and lower error rates. The network is made up of component local area networks, specifically Cambridge rings, which are connected either through local ring-ring bridges or through a high capacity satellite link. In order to take advantage of the characteristics of the resulting network, the protocols used are the same simple protocols as those used on a single Cambridge ring. This in turn allows many applications, which might have been thought of as local area network applications, to run on the larger network. Much of this work is concerned with an interconnection strategy which allows hosts of different component networks to communicate in a flexible manner without building an extra internetwork layer into protocol hierarchy. The strategy arrived at is neither a datagram approach nor a system of concatenated error and flow controlled virtual circuits. Rather, it is a lightweight virtual circuit approach which preserves the order of blocks sent on a circuit, but which makes no other guarantees about the delivery of these blocks. An extra internetwork protocol layer is avoided by modifying the system used on a single Cambridge ring which binds service names to addresses so that it now binds service names to routes across the network. Structural induction in LCF Paulson, Lawrence University of Cambridge, Computer Laboratory 1983-11 en Text UCAM-CL-TR-44 ISSN 1476-2986 Compound noun interpretation problems Spärck Jones, Karen University of Cambridge, Computer Laboratory 1983-07 en Text UCAM-CL-TR-45 ISSN 1476-2986 This paper discusses the problems of compound noun interpretation in the context of automatic language processing. Given that compound processing implies identifying the senses of the words involved, determining their bracketing, and establishing their underlying semantic relations, the paper illustrates the need, even in comparatively favourable cases, for inference using pragmatic information. This has consequences for language processor architectures and, even more, for speech processors. Intelligent network interfaces Garnett, Nicholas Henry University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-46 ISSN 1476-2986 Automatic summarising of English texts Tait, John Irving University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-47 ISSN 1476-2986 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 be fitted, allowing unexpected material to appear in output summary texts in an essentially unreduced form. The system’s summaries are in English. The program is based on technology not dissimilar to a script applier. However, Scrabble represents a significant advance over previous script-based summarising systems. It is much less likely to produce misleading summaries of an input text than some previous systems and can operate with less information about the subject domain of the input than others. These improvements are achieved by the use of three main novel ideas. First, the system incorporates a new method for identifying the idea or topics of an input text. Second, it allows a section of text to have more than one topic at a time, or at least a composite topic which may be dealt with by the computer program simultaneously applying the text predictions associated with more than one simple topic. Third, Scrabble incorporates new mechanisms for the incorporation of unexpected material in the input into its output summary texts. The incorporation of such material in the output summary is motivated by the view that it is precisely unexpected material which is likely to form the most salient matter in the input text. The performance of the system is illustrated by means of a number of example input texts and their Scrabble summaries. A mechanism for the accumulation and application of context in text processing Alshawi, Hiyan University of Cambridge, Computer Laboratory 1983-11 en Text UCAM-CL-TR-48 ISSN 1476-2986 The paper describes a mechanism for the representation and application of context information for automatic natural language processing systems. Context information is gathered gradually during the reading of the text, and the mechanism gives a way of combining the effect of several different types of context factors. Context factors can be managed independently, while still allowing efficient access to entities in focus. The mechanism is claimed to be more general than the global focus mechanism used by Grosz for discourse understanding. Context affects the interpretation process by choosing the results, and restricting the processing, of a number of important language interpretation operations, including lexical disambiguation and reference resolution. The types of context factors that have been implemented in an experimental system are described, and examples of the application of context are given. Programming language design with polymorphism Matthews, David Charles James University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-49 ISSN 1476-2986 Verifying the unification algorithm in LCF Paulson, Lawrence University of Cambridge, Computer Laboratory 1984-03 en Text UCAM-CL-TR-50 ISSN 1476-2986 Manna and Waldinger’s theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented in detail, as an example of interaction with LCF. Translating the theory into LCF’s domain-theoretic logic is largely straightforward. Well-founded induction on a complex ordering is translated into nested structural inductions. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. The verification is presented as a series of lemmas. The LCF proofs are compared with the original ones, and with other approaches. It appears difficult to find a logic that is both simple and flexible, especially for proving termination. Using information systems to solve recursive domain equations effectively Winskel, Glynn Larsen, Kim Guldstrand University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-51 ISSN 1476-2986 The design of a ring communication network Temple, Steven University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-52 ISSN 1476-2986 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 and make it an improvement over existing systems. In the case of the network described, the research was started to produce a network which was considerably faster than current designs, but which retained a high degree of generality. As the research progressed, other features were considered, such as ways to reduce the cost of the network and the ability to carry data traffic of many different types. The emphasis on high speed is still present but other aspects were considered and are discussed in the dissertation. The network has been named the Cambridge Fast Ring and and the network hardware is currently being implemented as an integrated circuit at the University of Cambridge Computer Laboratory. The aim of the dissertation is to describe the background to the design and the decisions which were made during the design process, as well as the design itself. The dissertation starts with a survey of the uses of local area networks and examines some established networks in detail. It then proceeds by examining the characteristics of a current network installation to assess what is required of the network in that and similar applications. The major design considerations for a high speed network controller are then discussed and a design is presented. Finally, the design of computer interfaces and protocols for the network is discussed. A new type-checker for a functional language Fairbairn, Jon University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-53 ISSN 1476-2986 Lessons learned from LCF Paulson, Lawrence University of Cambridge, Computer Laboratory 1984-08 en Text UCAM-CL-TR-54 ISSN 1476-2986 Executing temporal logic programs Moszkowski, Ben University of Cambridge, Computer Laboratory 1984-08 en Text UCAM-CL-TR-55 ISSN 1476-2986 A new scheme for writing functional operating systems Stoye, William University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-56 ISSN 1476-2986 Constructing recursion operators in intuitionistic type theory Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1984-10 en Text UCAM-CL-TR-57 ISSN 1476-2986 Martin-Löf’s Intuitionistic Theory of Types is becoming popular for formal reasoning about computer programs. To handle recursion schemes other than primitive recursion, a theory of well-founded relations is presented. Using primitive recursion over higher types, induction and recursion are formally derived for a large class of well-founded relations. Included are < on natural numbers, and relations formed by inverse images, addition, multiplication, and exponentiation of other relations. The constructions are given in full detail to allow their use in theorem provers for Type Theory, such as Nuprl. The theory is compared with work in the field of ordinal recursion over higher types. Categories of models for concurrency Winskel, Glynn University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-58 ISSN 1476-2986 On the composition and decomposition of assertions Winskel, Glynn University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-59 ISSN 1476-2986 Memory and context mechanisms for automatic text processing Alshawi, Hiyan University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-60 ISSN 1476-2986 User models and expert systems Spärck Jones, Karen University of Cambridge, Computer Laboratory 1984-12 en Text UCAM-CL-TR-61 ISSN 1476-2986 Constraint enforcement in a relational database management system Robson, Michael University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-62 ISSN 1476-2986 Poly manual Matthews, David C.J. University of Cambridge, Computer Laboratory 1985-02 en Text UCAM-CL-TR-63 ISSN 1476-2986 A framework for inference in natural language front ends to databases Boguraev, Branimir K. Spärck Jones, Karen University of Cambridge, Computer Laboratory 1985-02 en Text UCAM-CL-TR-64 ISSN 1476-2986 Introduction to the programming language “Ponder” Tillotson, Mark University of Cambridge, Computer Laboratory 1985-05 en Text UCAM-CL-TR-65 ISSN 1476-2986 A formal hardware verification methodology and its application to a network interface chip Gordon, M.J.C. Herbert, J. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-66 ISSN 1476-2986 Natural deduction theorem proving via higher-order resolution Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1985-05 en Text UCAM-CL-TR-67 ISSN 1476-2986 HOL : A machine oriented formulation of higher order logic Gordon, Mike University of Cambridge, Computer Laboratory 1985-07 en Text UCAM-CL-TR-68 ISSN 1476-2986 Proving termination of normalization functions for conditional expressions Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1985-06 en Text UCAM-CL-TR-69 ISSN 1476-2986 Boyer and Moore have discussed a recursive function that puts conditional expressions into normal form. It is difficult to prove that this function terminates on all inputs. Three termination proofs are compared: (1) using a measure function, (2) in domain theory using LCF, (3) showing that its “recursion relation”, defined by the pattern of recursive calls, is well-founded. The last two proofs are essentially the same though conducted in markedly different logical frameworks. An obviously total variant of the normalize function is presented as the ‘computational meaning’ of those two proofs. A related function makes nested recursive calls. The three termination proofs become more complex: termination and correctness must be proved simultaneously. The recursion relation approach seems flexible enough to handle subtle termination proofs where previously domain theory seemed essential. A remote procedure call system Hamilton, Kenneth Graham University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-70 ISSN 1476-2986 Executing temporal logic programs Moszkowski, Ben University of Cambridge, Computer Laboratory 1985-08 en Text UCAM-CL-TR-71 ISSN 1476-2986 Logic programming and the specification of circuits Clocksin, W.F. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-72 ISSN 1476-2986 Resource management in a distributed computing system Craft, Daniel Hammond University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-73 ISSN 1476-2986 Hardware verification by formal proof Gordon, Mike University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-74 ISSN 1476-2986 Design and implementation of a simple typed language based on the lambda-calculus Fairbairn, Jon University of Cambridge, Computer Laboratory 1985-05 en Text UCAM-CL-TR-75 ISSN 1476-2986 Despite the work of Landin and others as long ago as 1966, almost all recent programming languages are large and difficult to understand. This thesis is a re-examination of the possibility of designing and implementing a small but practical language based on very few primitive constructs. The text records the syntax and informal semantics of a new language called Ponder. The most notable features of the work are a powerful type-system and an efficient implementation of normal order reduction. In contrast to Landin’s ISWIM, Ponder is statically typed, an expedient that increases the simplicity of the language by removing the requirement that operations must be defined for incorrect arguments. The type system is a powerful extension of Milner’s polymorphic type system for ML in that it allows local quantification of types. This extension has the advantage that types that would otherwise need to be primitive may be defined. The criteria for the well-typedness of Ponder programmes are presented in the form of a natural deduction system in terms of a relation of generality between types. A new type checking algorithm derived from these rules is proposed. Ponder is built on the λ-calculus without the need for additional computation rules. In spite of this abstract foundation an efficient implementation based on Hughes’ super-combinator approach is described. Some evidence of the speed of Ponder programmes is included. The same strictures have been applied to the design of the syntax of Ponder, which, rather than having many pre-defined clauses, allows the addition of new constructs by the use of a simple extension mechanism. Preserving abstraction in concurrent programming Cooper, R.C.B. Hamilton, K.G. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-76 ISSN 1476-2986 Why higher-order logic is a good formalisation for specifying and verifying hardware Gordon, Mike University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-77 ISSN 1476-2986 A complete proof system for SCCS with model assertions Winskel, Glynn University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-78 ISSN 1476-2986 Petri nets, algebras and morphisms Winskel, Glynn University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-79 ISSN 1476-2986 It is shown how a category of Petri nets can be viewed as a subcategory of two sorted algebras over multisets. This casts Petri nets in a familiar framework and provides a useful idea of morphism on nets different from the conventional definition – the morphisms here respect the behaviour of nets. The categorical constructions with result provide a useful way to synthesise nets and reason about nets in terms of their components; for example various forms of parallel composition of Petri nets arise naturally from the product in the category. This abstract setting makes plain a useful functor from the category of Petri nets to a category of spaces of invariants and provides insight into the generalisations of the basic definition of Petri nets – for instance the coloured and higher level nets of Kurt Jensen arise through a simple modificationof the sorts of the algebras underlying nets. Further it provides a smooth formal relation with other models of concurrency such as Milner’s Calculus of Communicating Systems (CCS) and Hoare’s Communicating Sequential Processes (CSP). Interactive theorem proving with Cambridge LCF : A user's manual Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1985-11 en Text UCAM-CL-TR-80 ISSN 1476-2986 The implementation of functional languages using custom hardware Stoye, William Robert University of Cambridge, Computer Laboratory 1985-12 en Text UCAM-CL-TR-81 ISSN 1476-2986 In recent years functional programmers have produced a great many good ideas but few results. While the use of functional languages has been enthusiastically advocated, few real application areas have been tackled and so the functional programmer's views and ideas are met with suspicion. The prime cause of this state of affairs is the lack of widely available, solid implementations of functional languages. This in turn stems from two major causes: (1) Our understanding of implementation techniques was very poor only a few years ago, and so any implementation that is “mature” is also likely to be unuseably slow. (2) While functional languages are excellent for expressing algorithms, there is still considerable debate in the functional programming community over the way in which input and output operations should be represented to the programmer. Without clear guiding principles implementors have tended to produce ad-hoc, inadequate solutions. My research is concerned with strengthening the case for functional programming. To this end I constructed a specialised processor, called SKIM, which could evaluate functional programs quickly. This allowed experimentation with various implementation methods, and provided a high performance implementation with which to experiment with writing large functional programs. This thesis describes the resulting work and includes the following new results: (1) Details of a practical turner-style combinator reduction implementation featuring greatly improved storage use compared with previous methods. (2) An implementation of Kennaway’s director string idea that further enhances performance and increases understanding of a variety of reduction strategies. (3) Comprehensive suggestions concerning the representation of input, output, and nondeterministic tasks using functional languages, and the writing of operating systems. Details of the implementation of these suggestions developed on SKIM. (4) A number of observations concerning fuctional programming in general based on considerable practical experience. Natural deduction proof as higher-order resolution Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1985-12 en Text UCAM-CL-TR-82 ISSN 1476-2986 An interactive theorem prover, Isabelle, is under development. In LCF, each inference rule is represented by one function for forwards proof and another (a tactic) for backwards proof. In Isabelle, each inference rule is represented by a Horn clause. Resolution gives both forwards and backwards proof, supporting a large class of logics. Isabelle has been used to prove theorems in Martin-Löf’s Constructive Type Theory. Quantifiers pose several difficulties: substitution, bound variables, Skolemization. Isabelle’s representation of logical syntax is the typed lambda-calculus, requiring higher-order unification. It may have potential for logic programming. Depth-first search using inference rules constitutes a higher-order Prolog. Operation system design for large personal workstations Wilson, Ian David University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-83 ISSN 1476-2986 BSPL: a language for describing the behaviour of synchronous hardware Richards, Martin University of Cambridge, Computer Laboratory 1986-04 en Text UCAM-CL-TR-84 ISSN 1476-2986 Category theory and models for parallel computation Winskel, Glynn University of Cambridge, Computer Laboratory 1986-04 en Text UCAM-CL-TR-85 ISSN 1476-2986 This report will illustrate two uses of category theory: Firstly the use of category theory to define semantics in a particular model. How semantic constructions can often be seen as categorical ones, and, in particular, how parallel compositions are derived from a categorical product and a nun-deterministic sum. These categorical notions can provide a basis for reasoning about computations and will be illustrated for the model of Petri nets. Secondly, the use of category theory to relate different semantics will be examined; specifically, how the relations between various concrete models like Petri nets, event structures, trees and state machines are expressed as adjunctions. This will be illustrated by showing the coreflection between safe Petri nets and trees. The Entity System: an object based filing system Crawley, Stephen Christopher University of Cambridge, Computer Laboratory 1986-04 en Text UCAM-CL-TR-86 ISSN 1476-2986 Computer-aided type face design Carter, Kathleen Anne University of Cambridge, Computer Laboratory 1986-05 en Text UCAM-CL-TR-87 ISSN 1476-2986 A shallow processing approach to anaphor resolution Carter, David Maclean University of Cambridge, Computer Laboratory 1986-05 en Text UCAM-CL-TR-88 ISSN 1476-2986 Making form follow function : An exercise in functional programming style Fairbairn, Jon University of Cambridge, Computer Laboratory 1986-06 en Text UCAM-CL-TR-89 ISSN 1476-2986 The combined use of user-defined infix operators and higher order functions allows the programmer to invent new control structures tailored to a particular problem area. This paper is to suggest that such a combination has beneficial effects on the ease of both writing and reading programmes, and hence can increase programmer productivity. As an example, a parser for a simple language is presented in this style. It is hoped that the presentation will be palatable to people unfamiliar with the concepts of functional programming. The Cambridge Fast Ring networking system (CFR) Hopper, Andy Needham, Roger M. University of Cambridge, Computer Laboratory 1986-06 en Text UCAM-CL-TR-90 ISSN 1476-2986 Hardware verification using higher-order logic Camilleri, Albert Gordon, Mike Melham, Tom University of Cambridge, Computer Laboratory 1986-09 en Text UCAM-CL-TR-91 ISSN 1476-2986 The Hardware Verification Group at the University of Cambridge is investigating how various kinds of digital systems can be verified by mechanised formal proof. This paper explains our approach to representing behaviour and structure using higher order logic. Several examples are described including a ripple carry adder and a sequential device for computing the factorial function. The dangers of inaccurate models are illustrated with a CMOS exclusive-or gate. Implementation and programming techniques for functional languages Wray, Stuart Charles University of Cambridge, Computer Laboratory 1986-06 en Text UCAM-CL-TR-92 ISSN 1476-2986 Automated design of an instruction set for BCPL Bennett, J.P. University of Cambridge, Computer Laboratory 1986-06 en Text UCAM-CL-TR-93 ISSN 1476-2986 A mechanized proof of correctness of a simple counter Cohn, Avra Gordon, Mike University of Cambridge, Computer Laboratory 1986-06 en Text UCAM-CL-TR-94 ISSN 1476-2986 Event structures : Lecture notes for the Advanced Course on Petri Nets Winskel, Glynn University of Cambridge, Computer Laboratory 1986-07 en Text UCAM-CL-TR-95 ISSN 1476-2986 Event structures are a model of computational processes. They represent a process as a set of event occurrences with relations to express how events causally depend on others. This paper introduces event structures, shows their relationship to Scott domains and Petri nets, and surveys their role in denotational semantics, both for modelling laguages like CCS and CSP and languages with higher types. Models and logic of MOS circuits : Lectures for the Marktoberdorf Summerschool, August 1986 Winskel, Glynn University of Cambridge, Computer Laboratory 1986-10 en Text UCAM-CL-TR-96 ISSN 1476-2986 A study on abstract interpretation and “validating microcode algebraically” Mycroft, Alan University of Cambridge, Computer Laboratory 1986-10 en Text UCAM-CL-TR-97 ISSN 1476-2986 Power-domains, modalities and the Vietoris monad Robinson, E. University of Cambridge, Computer Laboratory 1986-10 en Text UCAM-CL-TR-98 ISSN 1476-2986 It is possible to divide the syntax-directed approaches to programming language semantics into two classes, “denotational”, and “proof-theoretic”. This paper argues for a different approach which also has the effect of linking the two methods. Drawing on recent work on locales as formal spaces we show that this provides a way in which we can hope to use a proof-theoretical semantics to give us a denotational one. This paper reviews aspects of the general theory, before developing a modal construction on locales and discussing the view of power-domains as free non-deterministic algebras. Finally, the relationship between the present work and that of Winskel is examined. An overview of the Poly programming language Matthews, David C.J. University of Cambridge, Computer Laboratory 1986-08 en Text UCAM-CL-TR-99 ISSN 1476-2986 Proving a computer correct in higher order logic Joyce, Jeff Birtwistle, Graham Gordon, Mike University of Cambridge, Computer Laboratory 1986-12 en Text UCAM-CL-TR-100 ISSN 1476-2986 Binary routing networks Milway, David Russel University of Cambridge, Computer Laboratory 1986-12 en Text UCAM-CL-TR-101 ISSN 1476-2986 A persistent storage system for Poly and ML Matthews, David C.J. University of Cambridge, Computer Laboratory 1987-01 en Text UCAM-CL-TR-102 ISSN 1476-2986 HOL : A proof generating system for higher-order logic Gordon, Mike University of Cambridge, Computer Laboratory 1987-01 en Text UCAM-CL-TR-103 ISSN 1476-2986 A proof of correctness of the Viper microprocessor: the first level Cohn, Avra University of Cambridge, Computer Laboratory 1987-01 en Text UCAM-CL-TR-104 ISSN 1476-2986 The Viper microprocessor designed at the Royal Signals and Radar Establishment (RSRE) is one of the first commercially produced computers to have been developed using modern formal methods. Viper is specified in a sequence of decreasingly abstract levels. In this paper a mechanical proof of the equivalence of the first two of these levels is described. The proof was generated using a version of Robin Milner’s LCF system. A compositional model of MOS circuits Winskel, Glynn University of Cambridge, Computer Laboratory 1987-04 en Text UCAM-CL-TR-105 ISSN 1476-2986 Abstraction mechanisms for hardware verification Melham, Thomas F. University of Cambridge, Computer Laboratory 1987-05 en Text UCAM-CL-TR-106 ISSN 1476-2986 DI-domains as a model of polymorphism Coquand, Thierry Gunter, Carl Winskel, Glynn University of Cambridge, Computer Laboratory 1987-05 en Text UCAM-CL-TR-107 ISSN 1476-2986 Workstation design for distributed computing Wilkes, Andrew John University of Cambridge, Computer Laboratory 1987-06 en Text UCAM-CL-TR-108 ISSN 1476-2986 This thesis discusses some aspects of the design of computer systems for local area networks (LANs), with particular emphasis on the way such systems present themselves to their users. Too little attention to this issue frequently results in computing environments that cannot be extended gracefully to accommodate new hardware or software and do not present consistent, uniform interfaces to either their human users or their programmatic clients. Before computer systems can become truly ubiquitous tools, these problems of extensibility and accessibility must be solved. This dissertation therefore seeks to examine one possible approach, emphasising support for program development on LAN based systems. Hardware verification of VLSI regular structures Joyce, Jeffrey University of Cambridge, Computer Laboratory 1987-07 en Text UCAM-CL-TR-109 ISSN 1476-2986 Relating two models of hardware Winskel, Glynn University of Cambridge, Computer Laboratory 1987-07 en Text UCAM-CL-TR-110 ISSN 1476-2986 Realism about user modelling Spärck Jones, K. University of Cambridge, Computer Laboratory 1987-06 en Text UCAM-CL-TR-111 ISSN 1476-2986 This paper reformulates the framework for user modelling presented in an earlier technical report, ‘User Models and Expert Systems’, and considers the implications of the real limitations on the knowledge likely to be available to a system for the value and application of user models. Reducing thrashing by adaptive backtracking Wolfram, D.A. University of Cambridge, Computer Laboratory 1987-08 en Text UCAM-CL-TR-112 ISSN 1476-2986 The representation of logics in higher-order logic Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1987-08 en Text UCAM-CL-TR-113 ISSN 1476-2986 An architecture for integrated services on the local area network Ades, Stephen University of Cambridge, Computer Laboratory 1987-09 en Text UCAM-CL-TR-114 ISSN 1476-2986 This dissertation concerns the provision of integrated services in a local area context, e.g. on business premises. The term integrated services can be understood at several levels. At the lowest, one network may be used to carry traffic of several media—voice, data, images etc. Above that, the telephone exchange may be replaced by a more versatile switching system, incorporating facilities such as stored voice messages. Its facilities may be accessible to the user through the interface of the workstation rather than a telephone. At a higher level still, new services such as multi-media document manipulation may be added to the capabilities of a workstation. Most of the work to date has been at the lowest of these levels, under the auspices of the Integrated Services Digital Network (ISDN), which mainly concerns wide area communications systems. The thesis presented here is that all of the above levels are important in a local area context. In an office environment, sophisticated data processing facilities in a workstation can usefully be combined with highly available telecommunications facilities such as the telephone, to offer the user new services which make the working day more pleasant and productive. That these facilities should be provided across one integrated network, rather than by several parallel single medium networks is an important organisational convenience to the system builder. The work described in this dissertation is relevant principally in a local area context—in the wide area economics and traffic balance dictate that the emphasis will be on only the network level of integration for some time now. The work can be split into three parts: i) the use of a packet network to carry mixed media. This has entailed design of packet voice protocols which produce delays low enough for the network to interwork with national telephone networks. The system has also been designed for minimal cost per telephone—packet-switched telephone systems have traditionally been more expensive than circuit-switched types. The network used as a foundation for this work has been the Cambridge Fast Ring. ii) use of techniques well established in distributed computing systems to build an ‘integrated services PABX (Private Automatic Branch Exchange)’. Current PABX designs have a very short life expectancy and an alarmingly high proportion of their costs is due to software. The ideas presented here can help with both of these problems, produce an extensible system and provide a basis for new multi-media services. iii) development of new user level Integrated Services. Work has been done in three areas. The first is multi-media documents. A voice editing interface is described along with the system structure required to support it. Secondly a workstation display has been built to support a variety of services based upon image manipulation and transmission. Finally techniques have been demonstrated by which a better interface to telephony functions can be provided to the user, using methods of control typical of workstation interfaces. Formal validation of an integrated circuit design style Dhingra, I.S. University of Cambridge, Computer Laboratory 1987-08 en Text UCAM-CL-TR-115 ISSN 1476-2986 Domain theoretic models of polymorphism Coquand, Thierry Gunter, Carl Winskel, Glynn University of Cambridge, Computer Laboratory 1987-09 en Text UCAM-CL-TR-116 ISSN 1476-2986 Distributed computing with RPC: the Cambridge approach Bacon, J.M. Hamilton, K.G. University of Cambridge, Computer Laboratory 1987-10 en Text UCAM-CL-TR-117 ISSN 1476-2986 The Cambridge Distributed Computing System (CDCS) is described and its evolution outlined. The Mayflower project allowed CDCS infrastructure, services and applications to be programmed in a high level, object oriented, language, Concurrent CLU. The Concurrent CLU RPC facility is described in detail. It is a non-transparent, type checked, type safe system which employs dynamic binding and passes objects of arbitrary graph structure. Recent extensions accomodate a number of languages and transport protocols. A comparison with other RPC schemes is given. Material concerning a study of cases Boguraev, B.K. Spärck Jones, K. University of Cambridge, Computer Laboratory 1987-05 en Text UCAM-CL-TR-118 ISSN 1476-2986 Pilgrim: a debugger for distributed systems Cooper, Robert University of Cambridge, Computer Laboratory 1987-07 en Text UCAM-CL-TR-119 ISSN 1476-2986 Block encryption Wheeler, D. University of Cambridge, Computer Laboratory 1987-11 en Text UCAM-CL-TR-120 ISSN 1476-2986 A fast and simple way of encrypting computer data is needed. The UNIX crypt is a good way of doing this although the method is not cryptographically sound for text. The method suggested here is applied to larger blocks than the DES method which uses 64 bit blocks, so that the speed of encyphering is reasonable. The algorithm is designed for software rather than hardware. This forgoes two advantages of the crypt algorithm, namely that each character can be encoded and decoded independently of other characters and that the identical process is used both for encryption and decryption. However this method is better for coding blocks directly. A high-level petri net specification of the Cambridge Fast Ring M-access service Billington, Jonathan University of Cambridge, Computer Laboratory 1987-12 en Text UCAM-CL-TR-121 ISSN 1476-2986 Temporal abstraction of digital designs Herbert, John University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-122 ISSN 1476-2986 Case study of the Cambridge Fast Ring ECL chip using HOL Herbert, John University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-123 ISSN 1476-2986 Formal verification of basic memory devices Herbert, John University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-124 ISSN 1476-2986 An operational semantics for Occam Camilleri, Juanito University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-125 ISSN 1476-2986 Reasoning about the function and timing of integrated circuits with Prolog and temporal logic Leeser, M.E. University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-126 ISSN 1476-2986 A development environment for large natural language grammars Carroll, John Boguraev, Bran Grover, Claire Briscoe, Ted University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-127 ISSN 1476-2986 Debugging concurrent and distributed programs Cooper, Robert Charles Beaumont University of Cambridge, Computer Laboratory 1988-02 en Text UCAM-CL-TR-128 ISSN 1476-2986 A methodology for automated design of computer instruction sets Bennett, Jeremy Peter University of Cambridge, Computer Laboratory 1988-03 en Text UCAM-CL-TR-129 ISSN 1476-2986 With semiconductor technology providing scope for increasingly complex computer architectures, there is a need more than ever to rationalise the methodology behind computer design. In the 1970’s, byte stream architectures offered a rationalisation of computer design well suited to microcoded hardware. In the 1980’s, RISC technology has emerged to simplify computer design and permit full advantage to be taken of very large scale integration. However, such approaches achieve their aims by simplifying the problem to a level where it is within the comprehension of a simple human being. Such an effort is not sufficient. There is a need to provide a methodology that takes the burden of design detail away from the human designer, leaving him free to cope with the underlying principles involved. In this dissertation I present a methodology for the design of computer instruction sets that is capable of automation in large part, removing the drudgery of individual instruction selection. The methodology does not remove the need for the designer’s skill, but rather allows precise refinement of his ideas to obtain an optimal instruction set. In developing this methodology a number of pieces of software have been designed and implemented. Compilers have been written to generate trial instruction sets. An instruction set generator program has been written and the instruction set it proposes evaluated. Finally a prototype language for instruction set design has been devised and implemented. The foundation of a generic theorem prover Paulson, Lawrence C University of Cambridge, Computer Laboratory 1988-03 en Text UCAM-CL-TR-130 ISSN 1476-2986 Isabelle is an interactive theorem prover that supports a variety of logics. It represents rules as propositions (not as functions) and builds proofs by combining rules. These operations constitute a meta-logic (or ‘logical framework’) in which the object-logics are formalized. Isabelle is now based on higher-order logic – a precise and well-understood foundation. Examples illustrate use of this meta-logic to formalize logics and proofs. Axioms for first-order logic are shown sound and complete. Backwards proof is formalized by meta-reasoning about object-level entailment. Higher-order logic has several practical advantages over other meta-logics. Many proof techniques are known, such as Huet’s higher-order unification procedure. Architecture problems in the construction of expert systems for document retrieval Spärck Jones, Karen University of Cambridge, Computer Laboratory 1986-12 en Text UCAM-CL-TR-131 ISSN 1476-2986 Reasoning about the function and timing of integrated circuits with Prolog and temporal logic Leeser, Miriam Ellen University of Cambridge, Computer Laboratory 1988-04 en Text UCAM-CL-TR-132 ISSN 1476-2986 A preliminary users manual for Isabelle Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1988-05 en Text UCAM-CL-TR-133 ISSN 1476-2986 This is an early report on the theorem prover Isabelle and several of its object-logics. It describes Isabelle’s operations, commands, data structures, and organization. This information is fairly low-level, but could benefit Isabelle users and implementors of other systems. Correctness properties of the Viper black model: the second level Cohn, Avra University of Cambridge, Computer Laboratory 1988-05 en Text UCAM-CL-TR-134 ISSN 1476-2986 Using reclusive types to reason about hardware in higher order logic Melham, Thomas F. University of Cambridge, Computer Laboratory 1988-05 en Text UCAM-CL-TR-135 ISSN 1476-2986 Formal specification and verification of asynchronous processes in higher-order logic Joyce, Jeffrey J. University of Cambridge, Computer Laboratory 1988-06 en Text UCAM-CL-TR-136 ISSN 1476-2986 We model the interaction of a synchronous process with an asynchronous memory process using a four-phase “handshaking” protocol. This example demonstrates the use of higher-order logic to reason about the behaviour of synchronous systems such as microprocessors which communicate requests to asynchronous devices and then wait for unpredictably long periods until these requests are answered. We also describe how our model could be revised to include some of the detailed timing requirements found in real systems such as the M68000 microprocessor. One enhancement uses non-determinism to model minimum setup times for asynchronous inputs. Experience with this example suggests that higher-order logic may also be a suitable formalism for reasoning about more abstract forms of concurrency. Mass terms and plurals : From linguistic theory to natural language processing Hasle, F.V. University of Cambridge, Computer Laboratory 1988-06 en Text UCAM-CL-TR-137 ISSN 1476-2986 Authentication: a practical study in belief and action Burrows, Michael Abadi, Martín Needham, Roger University of Cambridge, Computer Laboratory 1988-06 en Text UCAM-CL-TR-138 ISSN 1476-2986 Petri net theory: a survey Manson, Paul R. University of Cambridge, Computer Laboratory 1988-06 en Text UCAM-CL-TR-139 ISSN 1476-2986 The intense interest in concurrent (or “parallel”) computation over the past decade has given rise to a large number of languages for concurrent programming, representing many conflicting views of concurrency. The discovery that concurrent programming is significantly more difficult than sequential programming has prompted considerable research into determining a tractable and flexible theory of concurrency, with the aim of making concurrent processing more accessible, and indeed the wide variety of concurrent languages merely reflects the many different models of concurrency which have also been developed. This report, therefore introduces Petri nets, discussing their behaviour, interpretation and relationship to other models of concurrency. It defines and discusses several restrictions and extensions of the Petri net model, showing how they relate to basic Petri nets, while explaining why they have been of historical importance. Finally it presents a survey of the analysis methods applied to Petri nets in general and for some of the net models introduced here. Executing behavioural definitions in higher-order logic Camilleri, Albert John University of Cambridge, Computer Laboratory 1988-07 en Text UCAM-CL-TR-140 ISSN 1476-2986 Over the past few years, computer scientists have been using formal verification techniques to show the correctness of digital systems. The verification process, however, is complicated and expensive. Even proofs of simple circuits can involve thousands of logical steps. Often it can be extremely difficult to find correct device specifications and it is desirable that one sets off to prove a correct specification from the start, rather than repeatedly backtrack from the verification process to modify the original definitions after discovering they were incorrect or inadequate. The main idea presented in the thesis is to amalgamate the techniques of simulation and verification, rather than have the latter replace the former. The result is that behavioural definitions can be simulated until one is reasonably sure that the specification is correct. Furthermore, proving the correctness with respect to these simulated specifications avoids the inadequacies of simulation where it may not be computationally feasible to demonstrate correctness by exhaustive testing. Simulation here has a different purpose: to get specifications correct as early as possible in the verification process. Its purpose is not to demonstrate the correctness of the implementation – this is done in the verification stage when the very same specifications that were simulated are proved correct. The thesis discusses the implementation of an executable subset of the HOL logic, the version of Higher Order Logic embedded in the HOL theorem prover. It is shown that hardware can be effectively described using both relations and functions; relations being suitable for abstract specification and functions being suitable for execution. The difference between relational and functional specifications are discussed and illustrated by the verification of an n-bit adder. Techniques for executing functional specifications are presented and various optimisation strategies are shown which make the execution of the logic efficient. It is further shown that the process of generating optimised functional definitions from relational definitions can be automated. Example simulations of three hardware devices (a factorial machine, a small computer and a communications chip) are presented. Reliable management of voice in a distributed system Want, Roy University of Cambridge, Computer Laboratory 1988-07 en Text UCAM-CL-TR-141 ISSN 1476-2986 The ubiquitous personal computer has found its way into most office environments. As a result, widespread use of the Local Area Network (LAN) for the purposes of sharing distributed computing resources has become common. Another technology, the Private Automatic Branch Exchange (PABX), has benefited from large research and development by the telephone companies. As a consequence, it is cost effective and has widely infiltrated the office world. Its primary purpose is to switch digitised voice but, with the growing need for communication between computers it is also being adapted to switch data. However, PABXs are generally designed around a centralised switch in which bandwidth is permanently divided between its subscribers. Computing requirements need much larger bandwidths and the ability to connect to several services at once, thus making the conventional PABX unsuitable for this application. Some LAN technologies are suitable for switching voice and data. The additional requirement for voice is that point to point delay for network packets should have a low upper-bound. The 10 Mb/s Cambridge Ring is an example of this type of network, but is relatively low bandwidth gives it limited application in this area. Networks with larger bandwidths (up to 100 Mb/s) are now becoming available comercially and could support a realistic population of clients requiring voice and data communication. Transporting voice and data in the same network has two main advantages. Firstly, from a practical point of view, wiring is minimised. Secondly, applications which integrate both media are made possible, and hence digitised voice may be controlled by client programs in new and interesting ways. In addition to the new applications, the original telephony facilities must also be available. They should, at least by default, appear to work in an identical way to our tried and trusted impression of a telephone. However, the control and management of a network telephone is now in the domain of distributed computing. The voice connections between telephones are virtual circuits. Control and data information can be freely mixed with voice at a network interface. The new problems that result are the management issues related to the distributed control of real-time media. This thesis describes the issues as a distributed computing problem and proposes solutions, many of which have been demonstrated in a real implementation. Particular attention has been paid to the quality of service provided by the solutions. This amounts to the design of helpful operator interfaces, flexible schemes for the control of voice from personal workstations and, in particular, a high reliability factor for the backbone telephony service. This work demonstrates the advantages and the practicality of integrating voice and data services within the Local Area Network. A fast packet switch for the integrated services backbone network Newman, Peter University of Cambridge, Computer Laboratory 1988-07 en Text UCAM-CL-TR-142 ISSN 1476-2986 Experience with Isabelle : A generic theorem prover Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1988-08 en Text UCAM-CL-TR-143 ISSN 1476-2986 The theorem prover Isabelle is described briefly and informally. Its historical development is traced from Edinburgh LCF to the present day. The main issues are unification, quantifiers, and the representation of inference rules. The Edinburgh Logical Framework is also described, for a comparison with Isabelle. An appendix presents several Isabelle logics, including set theory and Constructive Type Theory, with examples of theorems. An operational semantics for occam Camilleri, Juanito University of Cambridge, Computer Laboratory 1988-08 en Text UCAM-CL-TR-144 ISSN 1476-2986 Mechanizing programming logics in higher order logic Gordon, Michael J.C. University of Cambridge, Computer Laboratory 1988-09 en Text UCAM-CL-TR-145 ISSN 1476-2986 Automating recursive type definitions in higher order logic Melham, Thomas F. University of Cambridge, Computer Laboratory 1988-09 en Text UCAM-CL-TR-146 ISSN 1476-2986 Formal specification and verification of microprocessor systems Joyce, Jeffrey University of Cambridge, Computer Laboratory 1988-09 en Text UCAM-CL-TR-147 ISSN 1476-2986 Extending coloured petri nets Billington, Jonathan University of Cambridge, Computer Laboratory 1988-09 en Text UCAM-CL-TR-148 ISSN 1476-2986 Jensen’s Coloured Petri Nets (CP-nets) are taken as the starting point for the development of a specification technique for complex concurrent systems. To increase its expressive power CP-nets are extended by including capacity and inhibitor functions. A class of extended CP-nets, known as P-nets, is defined that includes the capacity function and the threshold inhibitor extension. The inhibitor extension is defined in a totally symmetrical way to that of the usual pre place map (or incidence function). Thus the inhibitor and pre place maps may be equated by allowing a marking to be purged by a single transition occurrence, useful when specifying the abortion of various procedures. A chapter is devoted to developing the theory and notation for the purging of a place’s marking or part of its marking. Two transformations from P-nets to CP-nets are presented and it is proved that they preserve interleaving behaviour. These are based on the notion of complementary places defined for PT-nets and involve the definition and proof of a new extended complementary place invariant for CP-nets The graphical form of P-nets, known as a P-Graph, is presented formally and draws upon the theories developed for algebraic specification. Arc inscriptions are multiples of tuples of terms generated by a many-sorted signature. Transition conditions are Boolean expressions derived from the same signature. An interpretation of the P-Graph is given in terms of a corresponding P-net. The work is similar to that of Vautherin but includes the inhibitor and capacity extension and a number of significant differences. in the P-Graph concrete sets are associated with places, rather than sorts and likewise there are concrete initial marking and capacity functions. Vautherin associates equations with transitions rather than the more general Boolean expressions. P-Graphs are useful for specification at a concrete level. Classes of the P-Graph, known as Many-sorted Algebraic Nets and Many-sorted Predicate/Transition nets, are defined and illustrated by a number of examples. An extended place capacity notation is developed to allow for the convenient representation of resource bounds in the graphical form. Some communications-oriented examples are presented including queues and the Demon Game of international standards fame. The report concludes with a discussion of future work. In particular, an abstract P-Graph is defined that is very similar to Vautherin’s Petri net-like schema, but including the capacity and inhibitor extensions and associating boolean expressions with transitions. This will be useful for more abstract specifications (eg classes of communications protocols) and for their analysis. It is believed that this is the first coherent and formal presentation of these extensions in the literature. Improving security and performance of capability systems Karger, Paul Ashley University of Cambridge, Computer Laboratory 1988-10 en Text UCAM-CL-TR-149 ISSN 1476-2986 This dissertation examines two major limitations of capability systems: an inability to support security policies that enforce confinement and a reputation for relatively poor performance when compared with non-capability systems. The dissertation examines why conventional capability systems cannot enforce confinement and proposes a new secure capability architecture, called SCAP, in which confinement can be enforced. SCAP is based on the earlier Cambridge Capability System, CAP. The dissertation shows how a non-discretionary security policy can be implemented on the new architecture, and how the new architecture can also be used to improve traceability of access and revocation of access. The dissertation also examines how capability systems are vulnerable to discretionary Trojan horse attacks and proposes a defence based on rules built into the command-language interpreter. System-wide garbage collection, commonly used in most capability systems, is examined in the light of the non-discretionary security policies and found to be fundamentally insecure. The dissertation proposes alternative approaches to storage management to provide at least some of the benefits of system-wide garbage collection, but without the accompanying security problems. Performance of capability systems is improved by two major techniques. First, the doctrine of programming generality is addressed as one major cause of poor performance. Protection domains should be allocated only for genuine security reasons, rather than at every subroutine boundary. Compilers can better enforce modularity and good programming style without adding the expense of security enforcement to every subroutine call. Second, the ideas of reduced instruction set computers (RISC) can be applied to capability systems to simplify the operations required. The dissertation identifies a minimum set of hardware functions needed to obtain good performance for a capability system. This set is much smaller than previous research had indicated necessary. A prototype implementation of some of the capability features is described. The prototype was implemented on a re-microprogrammed VAX-11/730 computer. The dissertation examines the performance and software compatibility implications of the new capability architecture, both in the context of conventional computers, such as the VAX, and in the context of RISC processors. Simulation as an aid to verification using the HOL theorem prover Camilleri, Albert John University of Cambridge, Computer Laboratory 1988-10 en Text UCAM-CL-TR-150 ISSN 1476-2986 The HOL theorem proving system, developed by Mike Gordon at the University of Cambridge, is a mechanism of higher order logic, primarily intended for conducting formal proofs of digital system designs. In this paper we show that hardware specifications written in HOL logic can be executed to enable simulation as a means of supporting formal proof. Specifications of a small microprocessor are described, showing how HOL logic sentences can be transformed into executable code with minimum risk of introducing inconsistencies. A clean and effective optimisation strategy is recommended to make the executable specifications practical. Formalising an integrated circuit design style in higher order logic Dhingra, Inderpreel-Singh University of Cambridge, Computer Laboratory 1988-11 en Text UCAM-CL-TR-151 ISSN 1476-2986 Motion development for computer animation Pullen, Andrew Mark University of Cambridge, Computer Laboratory 1988-11 en Text UCAM-CL-TR-152 ISSN 1476-2986 Efficient data sharing Burrows, Michael University of Cambridge, Computer Laboratory 1988-12 en Text UCAM-CL-TR-153 ISSN 1476-2986 As distributed computing systems become widespread, the sharing of data between people using a large number of computers becomes more important. One of the most popular ways to facilitate this sharing is to provide a common file system, accessible by all the machines on the network. This approach is simple and reasonably effective, but the performance of the system can degrade significantly if the number of machines is increased. By using a hierarchical network, and arranging that machines typically access files stored in the same section of the network it is possible to build very large systems. However, there is still a limit on the number of machines that can share a single file server and a single network effectively. A good way to decrease network and server load is to cache file data on client machines, so that data need not be fetched from the centralized server each time it is accessed. This technique can improve the performance of a distributed file system and is used in a number of working systems. However, caching brings with it the overhead of maintaining consistency, or cache coherence. That is, each machine in the network must see the same data in its cache, even though one machine may be modifying the data as others are reading it. The problem is to maintain consistency without dramatically increasing the number of messages that must be passed between machines on the network. Some existing file systems take a probabilistic approach to consistency, some explicitly prevent the activities that can cause inconsistency, while others provide consistency only at the some cost in functionality or performance. In this dissertation, I examine how distributed file systems are typically used, and the degree to which caching might be expected to improve performance. I then describe a new file system that attempts to cache significantly more data than other systems, provides strong consistency guarantees, yet requires few additional messages for cache management. This new file-system provides fine-grain sharing of a file concurrently open on multiple machines on the network, at the granularity of a single byte. It uses a simple system of multiple-reader, single writer locks held in a centralized server to ensure cache consistency. The problem of maintaining client state in a centralized server are solved by using efficient data structures and crash recovery techniques. A natural language interface to an intelligent planning system Crabtree, I.B. Crouch, R.S. Moffat, D.C. Pirie, N.J. Pulman, S.G. Ritchie, G.D. Tate, B.A. University of Cambridge, Computer Laboratory 1989-01 en Text UCAM-CL-TR-154 ISSN 1476-2986 Computational morphology of English Pulman, S.G. Russell, G.J. Ritchie, G.D. Black, A.W. University of Cambridge, Computer Laboratory 1989-01 en Text UCAM-CL-TR-155 ISSN 1476-2986 This paper describes an implemented computer program which uses various kinds of linguistic knowledge to analyse existing or novel word forms in terms of their components. Three main types of knowledge are required (for English): knowledge about spelling or phonological changes consequent upon affixation (notice we are only dealing with isolated word forms); knowledge about the syntactic or semantic properties of affixation (i.e. inflexional and derivational morphology), and knowledge about the properties of the stored base forms of words (which in our case are always themselves words, rather than more abstract entities). These three types of information are stored as data files, represented in exactly the form a linguist might employ. These data files are then compiled by the system to produce a run-time program which will analyse arbitrary word forms presented to it in a way consistent with the original linguistic description. Events and VP modifiers Pulman, Steve University of Cambridge, Computer Laboratory 1989-01 en Text UCAM-CL-TR-156 ISSN 1476-2986 Introducing a priority operator to CCS Camilleri, Juanito University of Cambridge, Computer Laboratory 1989-01 en Text UCAM-CL-TR-157 ISSN 1476-2986 Tailoring output to the user: What does user modelling in generation mean? Spärck Jones, Karen University of Cambridge, Computer Laboratory 1988-08 en Text UCAM-CL-TR-158 ISSN 1476-2986 This paper examines the implications for linguistic output generation tailored to the interactive system user, of earlier analyses of the components of user modelling and of the constraints realism imposes on modelling. Using a range of detailed examples it argues that tailoring based only on the actual dialogue and on the decision model required for the system task is quite adequate, and that more ambitious modelling is both dangerous and unnecessary. Non-trivial power types can’t be subtypes of polymorphic types Pitts, Andrew M. University of Cambridge, Computer Laboratory 1989-01 en Text UCAM-CL-TR-159 ISSN 1476-2986 PFL+: A Kernal Scheme for Functions I/O Gordon, Andrew University of Cambridge, Computer Laboratory 1989-02 en Text UCAM-CL-TR-160 ISSN 1476-2986 Papers on Poly/ML Matthews, D.C.J. University of Cambridge, Computer Laboratory 1989-02 en Text UCAM-CL-TR-161 ISSN 1476-2986 The Alvey natural language tools grammar (2nd Release) Glover, Claire Briscoe, Ted Carroll, John Boguraev, Bran University of Cambridge, Computer Laboratory 1989-04 en Text UCAM-CL-TR-162 ISSN 1476-2986 Inference in a natural language front end for databases Copestake, Ann Spärck Jones, Karen University of Cambridge, Computer Laboratory 1989-02 en Text UCAM-CL-TR-163 ISSN 1476-2986 This report describes the implementation and initial testing of knowledge representation and inference capabilities within a modular database front end designed for transportability. A matrix key distribution system Gong, Li Wheeler, David J. University of Cambridge, Computer Laboratory 1988-10 en Text UCAM-CL-TR-164 ISSN 1476-2986 A new key distribution scheme is presented. It is based on the distinctive idea that lets each node have a set of keys of which it shares a distinct subset with every other node. This has the advantage that the numbers of keys that must be distributed and maintained are reduced by a square root factor; moreover, two nodes can start conversation with virtually no delay. Two versions of the scheme are given. Their performance and security analysis shows it is a practical solution to some key distribution problems. Fast packet switching for integrated services Newman, Peter University of Cambridge, Computer Laboratory 1989-03 en Text UCAM-CL-TR-165 ISSN 1476-2986 Evolution of operating system structures Bacon, Jean University of Cambridge, Computer Laboratory 1989-03 en Text UCAM-CL-TR-166 ISSN 1476-2986 A verified compiler for a verified microprocessor Joyce, Jeffrey J. University of Cambridge, Computer Laboratory 1989-03 en Text UCAM-CL-TR-167 ISSN 1476-2986 Distributed computing with a processor bank Bacon, J.M. Leslie, I.M. Needham, R.M. University of Cambridge, Computer Laboratory 1989-04 en Text UCAM-CL-TR-168 ISSN 1476-2986 Filing in a heterogeneous network Seaborne, Andrew Franklin University of Cambridge, Computer Laboratory 1989-04 en Text UCAM-CL-TR-169 ISSN 1476-2986 Ordered rewriting and confluence Martin, Ursula Nipkow, Tobias University of Cambridge, Computer Laboratory 1989-05 en Text UCAM-CL-TR-170 ISSN 1476-2986 Some types with inclusion properties in ∀, →, μ Fairbairn, Jon University of Cambridge, Computer Laboratory 1989-06 en Text UCAM-CL-TR-171 ISSN 1476-2986 This paper concerns the ∀, →, μ type system used in the non-strict functional programming language Ponder. While the type system is akin to the types of Second Order Lambda-calculus, the absence of type application makes it possible to construct types with useful inclusion relationships between them. To illustrate this, the paper contains definitions of a natural numbers type with many definable subtypes, and of a record type with inheritance. A theoretical framework for computer models of cooperative dialogue, acknowledging multi-agent conflict Galliers, Julia Rose University of Cambridge, Computer Laboratory 1989-07 en Text UCAM-CL-TR-172 ISSN 1476-2986 Programming in temporal logic Hale, Roger William Stephen University of Cambridge, Computer Laboratory 1989-07 en Text UCAM-CL-TR-173 ISSN 1476-2986 General theory relating to the implementation of concurrent symbolic computation Clarke, James Thomas Woodchurch University of Cambridge, Computer Laboratory 1989-08 en Text UCAM-CL-TR-174 ISSN 1476-2986 A formulation of the simple theory of types (for Isabelle) Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1989-08 en Text UCAM-CL-TR-175 ISSN 1476-2986 Simple type theory is formulated for use with the generic theorem prover Isabelle. This requires explicit type inference rules. There are function, product, and subset types, which may be empty. Descriptions (the eta-operator) introduce the Axiom of Choice. Higher-order logic is obtained through reflection between formulae and terms of type bool. Recursive types and functions can be formally constructed. Isabelle proof procedures are described. The logic appears suitable for general mathematics as well as computational problems. Implementing aggregates in parallel functional languages Clarke, T.J.W. University of Cambridge, Computer Laboratory 1989-08 en Text UCAM-CL-TR-176 ISSN 1476-2986 Experimenting with Isabelle in ZF Set Theory Noel, P.A.J. University of Cambridge, Computer Laboratory 1989-09 en Text UCAM-CL-TR-177 ISSN 1476-2986 Totally verified systems: linking verified software to verified hardware Joyce, Jeffrey J. University of Cambridge, Computer Laboratory 1989-09 en Text UCAM-CL-TR-178 ISSN 1476-2986 We describe exploratory efforts to design and verify a compiler for a formally verified microprocessor as one aspect of the eventual goal of building totally verified systems. Together with a formal proof of correctness for the microprocessor this yields a precise and rigorously established link between the semantics of the source language and the execution of compiled code by the fabricated microchip. We describe in particular: (1) how the limitations of real hardware influenced this proof; and (2) how the general framework provided by higher order logic was used to formalize the compiler correctness problem for a hierarchically structured language. Automating Squiggol Martin, Ursula Nipkow, Tobias University of Cambridge, Computer Laboratory 1989-09 en Text UCAM-CL-TR-179 ISSN 1476-2986 Formal verification of data type refinement : Theory and practice Nipkow, Tobias University of Cambridge, Computer Laboratory 1989-09 en Text UCAM-CL-TR-180 ISSN 1476-2986 Proof transformations for equational theories Nipkow, Tobias University of Cambridge, Computer Laboratory 1989-09 en Text UCAM-CL-TR-181 ISSN 1476-2986 The theory and implementation of a bidirectional question answering system Levine, John M. Fedder, Lee University of Cambridge, Computer Laboratory 1989-10 en Text UCAM-CL-TR-182 ISSN 1476-2986 The specification and verification of sliding window protocols in higher order logic Cardell-Oliver, Rachel University of Cambridge, Computer Laboratory 1989-10 en Text UCAM-CL-TR-183 ISSN 1476-2986 Site interconnection and the exchange architecture Tennenhouse, David Lawrence University of Cambridge, Computer Laboratory 1989-10 en Text UCAM-CL-TR-184 ISSN 1476-2986 Logics of Domains Zhang, Guo Qiang University of Cambridge, Computer Laboratory 1989-12 en Text UCAM-CL-TR-185 ISSN 1476-2986 Protocol design for high speed networks McAuley, Derek Robert University of Cambridge, Computer Laboratory 1990-01 en Text UCAM-CL-TR-186 ISSN 1476-2986 Improvements in fibre optic communication and in VLSI for network switching components have led to the consideration of building digital switched networks capable of providing point to point communication in the gigabit per second range. Provision of bandwidths of this magnitude allows the consideration of a whole new range of telecommunications services, integrating video, voice, image and text. These multi-service networks have a range of requirements not met by traditional network architectures designed for digital telephony or computer applications. This dissertation describes the design, and an implementation, of the Multi-Service Network architecture and protocol family, which is aimed at supporting these services. Asynchronous transfer mode networks provide the basic support required for these integrated services, and the Multi-Service Network architecture is designed primarily for these types of networks. The aim of the Multi-Service protocol family is to provide a complete architecture which allows use of the full facilities of asynchronous transfer mode networks by multi-media applications. To maintain comparable performance with the underlying media, certain elements of the MSN protocol stack are designed with implementation in hardware in mind. The interconnection of heterogeneous networks, and networks belonging to different security and administrative domains, is considered vital, so the MSN architecture takes an internetworking approach. Natural language interfaces to databases Copestake, Ann Spärck Jones, Karen University of Cambridge, Computer Laboratory 1989-09 en Text UCAM-CL-TR-187 ISSN 1476-2986 Specification of computer architectures: a survey and annotated bibliography Leonard, Timothy E. University of Cambridge, Computer Laboratory 1990-01 en Text UCAM-CL-TR-188 ISSN 1476-2986 Isabelle tutorial and user’s manual Paulson, Lawrence C. Nipkow, Tobias University of Cambridge, Computer Laboratory 1990-01 en Text UCAM-CL-TR-189 ISSN 1476-2986 This (obsolete!) manual describes how to use the theorem prover Isabelle. For beginners, it explains how to perform simple single-step proofs in the built-in logics. These include first-order logic, a classical sequent calculus, ZF set theory, Constructie Type Theory, and higher-order logic. Each of these logics is described. The manual then explains how to develop advanced tactics and tacticals and how to derive rules. Finally, it describes how to define new logics within Isabelle. Some notes on mass terms and plurals Copestake, Ann University of Cambridge, Computer Laboratory 1990-01 en Text UCAM-CL-TR-190 ISSN 1476-2986 An architecture for real-time multimedia communications systems Nicolaou, Cosmos University of Cambridge, Computer Laboratory 1990-02 en Text UCAM-CL-TR-191 ISSN 1476-2986 An architecture for real-time multimedia communications systems is presented. A multimedia communication systems includes both the communication protocols used to transport the real-time data and also the Distributed Computing system (DCS) within which any applications using these protocols must execute. The architecture presented attempts to integrate these protocols with the DCS in a smooth fashion in order to ease the writing of multimedia applications. Two issues are identified as being essential to the success of this integration: namely the synchronisation of related real-time data streams, and the management of heterogeneous multimedia hardware. The synchronisation problem is tackled by defining explicit synchronisation properties at the presentation level and by providing control and synchronisation operations within the DCS which operate in terms of these properties. The heterogeneity problems are addressed by separating the data transport semantics (protocols themselves) from the control semantics (protocol interfaces). The control semantics are implemented using a distributed, typed interface, scheme within the DCS (i.e. above the presentation layer), whilst the protocols themselves are implemented within the communication subsystem. The interface between the DCS and communications subsystem is referred to as the orchestration interface and can be considered to lie in the presentation and session layers. A conforming prototype implementation is currently under construction. Designing a theorem prover Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1990-05 en Text UCAM-CL-TR-192 ISSN 1476-2986 The methods and principles of theorem prover design are presented through an extended example. Starting with a sequent calculus for first-order logic, an automatic prover (called Folderol) is developed. Folderol can prove quite a few complicated theorems, although its search strategy is crude and limited. Folderol is coded in Standard ML and consists largely of pure functions. Its complete listing is included. The report concludes with a survey of other research in theorem proving: the Boyer/Moore theorem prover, Automath, LCF, and Isabelle. Belief revision and a theory of communication Galliers, Julia Rose University of Cambridge, Computer Laboratory 1990-05 en Text UCAM-CL-TR-193 ISSN 1476-2986 Proceedings of the First Belief Representation and Agent Architectures Workshop Galliers, Julia Rose University of Cambridge, Computer Laboratory 1990-03 en Text UCAM-CL-TR-194 ISSN 1476-2986 Multi-level verification of microprocessor-based systems Joyce, Jeffrey J. University of Cambridge, Computer Laboratory 1990-05 en Text UCAM-CL-TR-195 ISSN 1476-2986 The semantics of VHDL with Val and Hol: towards practical verification tools Van Tassell, John Peter University of Cambridge, Computer Laboratory 1990-06 en Text UCAM-CL-TR-196 ISSN 1476-2986 The semantics and implementation of aggregates : or : how to express concurrency without destroying determinism Clarke, Thomas University of Cambridge, Computer Laboratory 1990-07 en Text UCAM-CL-TR-197 ISSN 1476-2986 Evaluation Logic Pitts, Andrew M. University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-198 ISSN 1476-2986 The HOL verification of ELLA designs Boulton, Richard Gordon, Mike Herbert, John Van Tassel, John University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-199 ISSN 1476-2986 HOL is a public domain system for generating proofs in higher order predicate calculus. It has been in experimental and commercial use in several countries for a number of years. ELLA is a hardware design language developed at the Royal Signals and Radar Establishment (RSRE) and marketed by Computer General Electronic Design. It supports simulation models at a variety of different abstraction levels. A preliminary methodology for reasoning about ELLA designs using HOL is described. Our approach is to semantically embed a subset of the ELLA language in higher order logic, and then to make this embedding convenient to use with parsers and pretty-printers. There are a number of semantic issues that may affect the ease of verification. We discuss some of these briefly. We also give a simple example to illustrate the methodology. Type classes and overloading resolution via order-sorted unification Nipkow, Tobias Snelting, Gregor University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-200 ISSN 1476-2986 Formalizing abstraction mechanisms for hardware verification in higher order logic Melham, Thomas Frederick University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-201 ISSN 1476-2986 Recent advances in microelectronics have given designers of digital hardware the potential to build devices of remarkable size and complexity. Along with this however, it becomes increasingly difficult to ensure that such systems are free from design errors, where complete simulation of even moderately sized circuits is impossible. One solution to these problems is that of hardware verification, where the functional behaviour of the hardware is described mathematically and formal proof is used to show that the design meets rigorous specifications of the intended operation. This dissertation therefore seeks to develop this, showing how reasoning about the correctness of hardware using formal proof can be achieved using fundamental abstraction mechanisms to relate specifications of hardware at different levels. Therefore a systematic method is described for defining any instance of a wide class of concrete data types in higher order logic. This process has been automated in the HOL theorem prover, and provides a firm logical basis for representing data in formal specifications. Further, these abstractions have been developed into a new technique for modelling the behaviour of entire classes of hardware designs. This is based on a formal representation in logic for the structure of circuit designs using the recursive types defined by the above method. Two detailed examples are presented showing how this work can be applied in practice. Finally, some techniques for temporal abstraction are explained, and the means for asserting the correctness of a model containing time-dependent behaviour is described. This work is then illustrated using a case study; the formal verification on HOL of a simple ring communication network. [Abstract by Nicholas Cutler (librarian), as none was submitted with the report.] Three-dimensional integrated circuit layout Harter, Andrew Charles University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-202 ISSN 1476-2986 Subtyping in Ponder (preliminary report) de Paiva, Valeria C.V. University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-203 ISSN 1476-2986 This note starts the formal study of the type system of the functional language Ponder. Some of the problems of proving soundness and completeness are discussed and some preliminary results, about fragments of the type system, shown. It consists of 6 sections. In section 1 we review briefly Ponder’s syntax and describe its typing system. In section 2 we consider a very restricted fragment of the language for which we can prove soundness of the type inference mechanism, but not completeness. Section 3 describes possible models of this fragment and some related work. Section 4 describes the type-inference algorithm for a larger fragment of Ponder and in section 5 we come up against some problematic examples. Section 6 is a summary of further work. New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic Crole, Roy L. Pitts, Andrew M. University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-204 ISSN 1476-2986 Logic programming, functional programming and inductive definitions Paulson, Lawrence C. Smith, Andrew W. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-205 ISSN 1476-2986 This paper reports an attempt to combine logic and functional programming. It also questions the traditional view that logic programming is a form of first-order logic, arguing instead that the essential nature of a logic program is an inductive definition. This revised view of logic programming suggests the design of a combined logic/functional language. A slow but working prototype is described. Formal verification of real-time protocols using higher order logic Cardell-Oliver, Richard University of Cambridge, Computer Laboratory 1990-08 en Text UCAM-CL-TR-206 ISSN 1476-2986 Video replay in computer animation Hawkins, Stuart Philip University of Cambridge, Computer Laboratory 1990-10 en Text UCAM-CL-TR-207 ISSN 1476-2986 Categorical combinators for the calculus of constructions Ritter, Eike University of Cambridge, Computer Laboratory 1990-10 en Text UCAM-CL-TR-208 ISSN 1476-2986 Efficient memory-based learning for robot control Moore, Andrew William University of Cambridge, Computer Laboratory 1990-11 en Text UCAM-CL-TR-209 ISSN 1476-2986 This dissertation is about the application of machine learning to robot control. A system which has no initial model of the robot/world dynamics should be able to construct such a model using data received through its sensors—an approach which is formalized here as the SAB (State-Action-Behaviour) control cycle. A method of learning is presented in which all the experiences in the lifetime of the robot are explicitly remembered. The experiences are stored in a manner which permits fast recall of the closest previous experience to any new situation, thus permitting very quick predictions of the effects of proposed actions and, given a goal behaviour, permitting fast generation of a candidate action. The learning can take place in high-dimensional non-linear control spaces with real-valued ranges of variables. Furthermore, the method avoids a number of shortcomings of earlier learning methods in which the controller can become trapped in inadequate performance which does not improve. Also considered is how the system is made resistant to noisy inputs and how it adapts to environmental changes. A well founded mechanism for choosing actions is introduced which solves the experiment/perform dilemma for this domain with adequate computational efficiency, and with fast convergence to the goal behaviour. The dissertation explains in detail how the SAB control cycle can be integrated into both low and high complexity tasks. The methods and algorithms are evaluated with numerous experiments using both real and simulated robot domains. The final experiment also illustrates how a compound learning task can be structured into a hierarchy of simple learning tasks. Higher-order unification, polymorphism, and subsorts Nipkow, Tobias University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-210 ISSN 1476-2986 The role of artificial intelligence in information retrieval Spärck Jones, Karen University of Cambridge, Computer Laboratory 1990-11 en Text UCAM-CL-TR-211 ISSN 1476-2986 A distributed and-or parallel Prolog network Wrench, K.L. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-212 ISSN 1476-2986 The Dialectica categories de Paiva, Valeria Correa Vaz University of Cambridge, Computer Laboratory 1991-01 en Text UCAM-CL-TR-213 ISSN 1476-2986 This work consists of two main parts. The first one, which gives it its name, presents an internal categorical version of Gödel’s “Dialectica interpretation” of higher-order arithmetic. The idea is to analyse the Dialectica interpretation using a cetegory DC where objects are relations on objects of a basic category C and maps are pairs of maps of C satisfying a pullback condition. If C is finitely complete, DC exists and has a very natural symmetric monoidal structure. If C is locally cartesian closed then DC is symmetric monoidal closed. If we assume C with stable and disjoint coproducts, DC has cartesian products and weak-coproducts and satisfies a weak form of distributivity. Using the structure above, DC is a categorical model for intuitionistic linear logic. Moreover if C has free monoids then DC has cofree comonoids and the corresponding comonad “!” on DC, which has some special properties, can be used to model the exponential “of course!” in Intuitionistic Linear Logic. The category of “!”-coalgebras is isomorphic to the category of comonoids in DC and, if we assume commutative monoids in C, the “!”-Kleisli category, which is cartesian closed, corresponds to the Diller-Nahm variant of the Dialectica interpretation. The second part introduces the categories GC. The objects of GC are the same objects of DC, but morphisms are easier to handle, since they are maps in C in opposite directions. If C is finitely complete, the category GC exists. If C is cartesian closed, we can define a symmetric monoidal structure and if C is locally cartesian closed as well, we can define inernal homs in GC that make it a symmetric monoidal closed category. Supposing C with stable and disjoint coproducts, we can define cartesian products and coproducts in GC and, more interesting, we can define a dual operation to the tensor product bifunctor, called “par”. The operation “par” is a bifunctor and has a unit “⊥”, which is a dualising object. Using the internal hom and ⊥ we define a contravariant functor “(−)⊥” which behaves like negation and thus it is used to model linear negation. We show that the category GC, with all the structure above, is a categorical model for Linear Logic, but not exactly the classical one. In the last chapter a comonad and a monad are defined to model the exponentials “!” and “?”. To define these endofunctors, we use Beck’s distributive laws in an interesting way. Finally, we show that the Kleisli category GC! is cartesian closed and that the categories DC and GC are related by a Kleisli construction. Integrating knowledge of purpose and knowledge of structure for design evaluation Bradshaw, J.A. Young, R.M. University of Cambridge, Computer Laboratory 1991-02 en Text UCAM-CL-TR-214 ISSN 1476-2986 A structured approach to the verification of low level microcode Curzon, Paul University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-215 ISSN 1476-2986 Errors in microprograms are especially serious since all higher level programs on the machine depend on the microcode. Formal verification presents one avenue which may be used to discover such errors. Previous systems which have been used for formally verifying microcode may be categorised by the form in which the microcode is supplied. Some demand that it be written in a high level microprogramming language. Conventional software verification techniques are then applied. Other methods allow the microcode to be supplied in the form of a memory image. It is treated as data to an interpreter modelling the behaviour of the microarchitecture. The proof is then performed by symbolic execution. A third solution is for the code to be supplied in an assembly language and modelled at that level. The assembler instructions are converted to commands in a modelling language. The resulting program is verified using traditional software verification techniques. In this dissertation I present a new universal microprogram verification system. It achieves many of the advantages of the other kinds of systems by adopting a hybrid approach. The microcode is supplied as a memory image, but it is transformed by the system to a high level program which may be verified using standard software verification techniques. The structure of the high level program is obtained from user supplied documentation. I show that this allows microcode to be split into small, independently validatable portions even when it was not written in that way. I also demonstrate that the techniques allow the complexity of detail due to the underlying microarchitecture to be controlled at an early stage in the validation process. I suggest that the system described would combine well with other validation tools and provide help throughout the firmware development cycle. Two case studies are given. The first describes the verification of Gordon’s computer. This example being fairly simple, provides a good illustration of the techniques used by the system. The second case study is concerned with the High Level Hardware Orion computer which is a commercially produced machine with a fairly complex microarchitecture. This example shows that the techniques scale well to production microarchitectures. Exploiting OR-parallelism in Prolog using multiple sequential machines Klein, Carole Susan University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-216 ISSN 1476-2986 Dynamic bandwidth management Harita, Bhaskar Ramanathan University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-217 ISSN 1476-2986 Higher-order critical pairs Nipkow, Tobias University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-218 ISSN 1476-2986 Fairisle project working documents : Snapshot 1 Leslie, Ian M. McAuley, Derek M. Hayter, Mark Black, Richard Beller, Reto Newman, Peter Doar, Matthew University of Cambridge, Computer Laboratory 1991-03 en Text UCAM-CL-TR-219 ISSN 1476-2986 A distributed architecture for multimedia communication systems Nicolaou, Cosmos Andrea University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-220 ISSN 1476-2986 Transforming axioms for data types into sequential programs Milne, Robert University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-221 ISSN 1476-2986 A process is proposed for refining specifications of abstract data types into efficient sequential implementations. The process needs little manual intervention. It is split into three stages, not all of which need always be carried out. The three stages entail interpreting equalities as behavioural equivalences, converting functions into procedures and replacing axioms by programs. The stages can be performed as automatic transformations which are certain to produce results that meet the specifications, provided that simple conditions hold. These conditions describe the adequacy of the specifications, the freedom from interference between the procedures, and the mode of construction of the procedures. Sufficient versions of these conditions can be checked automatically. Varying the conditions could produce implementations for different classes of specification. Though the transformations could be automated, the intermediate results, in styles of specification which cover both functions and procedures, have interest in their own right and may be particularly appropriate to object-oriented design. Extensions to coloured petri nets and their application to protocols Billington, Jonathan University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-222 ISSN 1476-2986 Shallow processing and automatic summarising: a first study Gladwin, Philip Pulman, Stephen Spärck Jones, Karen University of Cambridge, Computer Laboratory 1991-05 en Text UCAM-CL-TR-223 ISSN 1476-2986 Generalised probabilistic LR parsing of natural language (corpora) with unification-based grammars Briscoe, Ted Carroll, John University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-224 ISSN 1476-2986 Categorical multirelations, linear logic and petri nets (draft) de Paiva, Valeria University of Cambridge, Computer Laboratory 1991-05 en Text UCAM-CL-TR-225 ISSN 1476-2986 This note presents a categorical treatment of multirelations, which is, in a loose sense a generalisation of both our previous work on the categories GC, and of Chu’s construction A_NC [Barr’79]. The main motivation for writing this note was the utilisation of the category GC by Brown and Gurr [BG90] to model Petri nets. We wanted to extend their work to deal with multirelations, as Petri nets are usually modelled using multirelations pre and post. That proved easy enough and people interested mainly in concurrency theory should refer to our joint work [BGdP’91], this note deals with the mathematics underlying [BGdP’91]. The upshot of this work is that we build a model of Intuitionistic Linear Logic (without modalities) over any symmetric monoidal category C with a distinguished object (N, ≤, ∘, e −∘) – a closed poset. Moreover, if the category C is cartesian closed with free monoids, we build a model of Intuitionistic Linear Logic with a non-trivial modality ‘!’ over it. A new approach for improving system availability Lam, Kwok-yan University of Cambridge, Computer Laboratory 1991-06 en Text UCAM-CL-TR-226 ISSN 1476-2986 Priority in process calculi Camilleri, Juanito Albert University of Cambridge, Computer Laboratory 1991-06 en Text UCAM-CL-TR-227 ISSN 1476-2986 The desk area network Hayter, Mark McAuley, Derek University of Cambridge, Computer Laboratory 1991-05 en Text UCAM-CL-TR-228 ISSN 1476-2986 A novel architecture for use within an end computing system is described. This attempts to extend the concepts used in modern high speed networks into computer system design. A multimedia workstation is being built based on this concept to evaluate the approach. Abstraction of image and pixel : The thistle display system Brown, David J. University of Cambridge, Computer Laboratory 1991-08 en Text UCAM-CL-TR-229 ISSN 1476-2986 Proceedings of the second belief representation and agent architectures workshop (BRAA ’91) Galliers, J. University of Cambridge, Computer Laboratory 1991-08 en Text UCAM-CL-TR-230 ISSN 1476-2986 Managing the order of transactions in widely-distributed data systems Yahalom, Raphael University of Cambridge, Computer Laboratory 1991-08 en Text UCAM-CL-TR-231 ISSN 1476-2986 Mechanising set theory Corella, Francisco University of Cambridge, Computer Laboratory 1991-07 en Text UCAM-CL-TR-232 ISSN 1476-2986 Set theory is today the standard foundation of mathematics, but most proof development sysems (PDS) are based on type theory rather than set theory. This is due in part to the difficulty of reducing the rich mathematical vocabulary to the economical vocabulary of the set theory. It is known how to do this in principle, but traditional explanations of mathematical notations in set theoretic terms do not lead themselves easily to mechanical treatment. We advocate the representation of mathematical notations in a formal system consisting of the axioms of any version of ordinary set theory, such as ZF, but within the framework of higher-order logic with λ-conversion (H.O.L.) rather than first-order logic (F.O.L.). In this system each notation can be represented by a constant, which has a higher-order type when the notation binds variables. The meaning of the notation is given by an axiom which defines the representing constant, and the correspondence between the ordinary syntax of the notation and its representation in the formal language is specified by a rewrite rule. The collection of rewrite rules comprises a rewriting system of a kind which is computationally well behaved. The formal system is justified by the fact than set theory within H.O.L. is a conservative extension of set theory within F.O.L. Besides facilitating the representation of notations, the formal system is of interestbecause it permits the use of mathematical methods which do not seem to be available in set theory within F.O.L. A PDS, called Watson, has been built to demonstrate this approach to the mechanization of mathematics. Watson embodies a methodology for interactive proof which provides both flexibility of use and a relative guarantee of correctness. Results and proofs can be saved, and can be perused and modified with an ordinary text editor. The user can specify his own notations as rewrite rules and adapt the mix of notations to suit the problem at hand; it is easy to switch from one set of notations to another. As a case study, Watson has been used to prove the correctness of a latch implemented as two cross-coupled nor-gates, with an approximation of time as a continuum. A development environment for large natural language grammars Carroll, John Briscoe, Ted Grover, Claire University of Cambridge, Computer Laboratory 1991-07 en Text UCAM-CL-TR-233 ISSN 1476-2986 Two tutorial papers: Information retrieval & Thesaurus Spärck Jones, Karen University of Cambridge, Computer Laboratory 1991-08 en Text UCAM-CL-TR-234 ISSN 1476-2986 The first paper describes the characteristics of information retrieval from documents or texts, the development and status of automatic indexing and retrieval, and the actual and potential relations between information retrieval and artificial intelligence. The second paper discusses the properties, construction and actual and potential uses of thesauri, as semantic classifications or terminological knowledge bases, in information retrieval and natural language processing. Modelling and image generation Wang, Heng University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-235 ISSN 1476-2986 Using knowledge of purpose and knowledge of structure as a basic for evaluating the behaviour of mechanical systems Bradshaw, John Anthony University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-236 ISSN 1476-2986 Computing presuppositions in an incremantal language processing system Bridge, Derek G. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-237 ISSN 1476-2986 Proceedings of the ACQUILEX workshop on default inheritance in the lexicon Briscoe, Ted Copestake, Ann de Paiva, Valeria University of Cambridge, Computer Laboratory 1991-10 en Text UCAM-CL-TR-238 ISSN 1476-2986 Planning multisentential English text using communicative acts Maybury, Mark Thomas University of Cambridge, Computer Laboratory 1991-12 en Text UCAM-CL-TR-239 ISSN 1476-2986 The goal of this research is to develop explanation presentation mechanisms for knowledge based systems which enable them to define domain terminology and concepts, narrate events, elucidate plans, processes, or propositions and argue to support a claim or advocate action. This requires the development of devices which select, structure, order and then linguistically realize explanation content as coherent and cohesive English text. With the goal of identifying generic explanation presentation strategies, a wide range of naturally occurring texts were analyzed with respect to their communicative structure, function, content and intended effects on the reader. This motivated an integrated theory of communicative acts which characterizes text at the level of rhetorical acts (e.g. describe, define, narrate), illocutionary acts (e.g. inform, request), and locutionary acts (ask, command). Taken as a whole, the identified communicative acts characterize the structure, content and intended effects of four types of text: description, narration, exposition, argument. These text types have distinct effects such as getting the reader to know about entities, to know about events, to understand plans, processes, or propositions, or to believe propositions or want to perform actions. In addition to identifying the communicative function and effect of text at multiple levels of abstraction, this dissertation details a tripartite theory of focus of attention (discourse focus, temporal focus and spatial focus) which constrains the planning and linguistic realization of text. To test the integrated theory of communicative acts and tripartite theory of focus of attention, a text generation system TEXPLAN (Textual EXplanation PLANner) was implemented that plans and linguistically realizes multisentential and multiparagraph explanations from knowledge based systems. The communicative acts identified during text analysis were formalized over sixty compositional and (in some cases) recursive plan operators in the library of a hierarchical planner. Discourse, temporal and spatial models were implemented to track and use attentional information to guide the organization and realization of text. Because the plan operators distinguish between the communicative function (e.g. argue for a proposition) and the expected effect (e.g. the reader believes the proposition) of communicative acts, the system is able to construct a discourse model of the structure and function of its textual responses as well as a user model of the expected effects of its responses on the reader’s knowledge, beliefs, and desires. The system uses both the discourse model and user model to guide subsequent utterances. To test its generality, the system was interfaced to a variety of domain applications including a neuropsychological diagnosis system, a mission planning system, and a knowledge based mission simulator. The system produces descriptions, narratives, expositions and arguments from these applications, thus exhibiting a broader ranger of rhetorical coverage then previous text generation systems. Symbolic compilation and execution of programs by proof: a case study in HOL Camilleri, Juanito University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-240 ISSN 1476-2986 Learning in large state spaces with an application to biped robot walking Vogel, Thomas Ulrich University of Cambridge, Computer Laboratory 1991-12 en Text UCAM-CL-TR-241 ISSN 1476-2986 An object oriented approach to virtual memory management Mapp, Glenford Ezra University of Cambridge, Computer Laboratory 1992-01 en Text UCAM-CL-TR-242 ISSN 1476-2986 Advances in computer technology are being pooled together to form a new computing environment which is characterised by powerful workstations with vast amounts of memory connected to high speed networks. This environment will provide a large number of diverse services such as multimedia communications, expert systems and object-oriented databases. In order to develop these complex applications in an efficient manner, new interfaces are required which are simple, fast and flexible and allow the programmer to use an object-oriented approach throughout the design and implementation of an application. Virtual memory techniques are increasingly being used to build these new facilities. In addition since CPU speeds continue to increase faster than disk speeds, an I/O bottleneck may develop in which the CPU may be idle for long periods waiting for paging requests to be satisfied. To overcome this problem it is necessary to develop new paging algorithms that better reflect how different objects are used. Thus a facility to page objects on a per-object basis is required and a testbed is also needed to obtain experimental data on the paging activity of different objects. Virtual memory techniques, previously only used in mainframe and minicomputer architectures, are being employed in the memory management units of modern microprocessors. With very large address spaces becoming a standard feature of most systems, the use of memory mapping is seen as an effective way of providing greater flexibility as well as improved system efficiency. This thesis presents an object-oriented interface for memory mapped objects. Each object has a designated object type. Handles are associated with different object types and the interface allows users to define and manage new object types. Moving data between the object and its backing store is done by user-level processes called object managers. Object managers interact with the kernel via a specified interface thus allowing users to build their own object managers. A framework to compare different algorithms was also developed and an experimental testbed was designed to gather and analyse data on the paging activity of various programs. Using the testbed, conventional paging algorithms were applied to different types of objects and the results were compared. New paging algorithms were designed and implemented for objects that are accessed in a highly sequential manner. Automating the librarian: a fundamental approach using belief revision Cawsey, Alison Galliers, Julia Reece, Stenev Spärck Jones, Karen University of Cambridge, Computer Laboratory 1992-01 en Text UCAM-CL-TR-243 ISSN 1476-2986 A mechanized theory of the π-calculus in HOL Melham, T.F. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-244 ISSN 1476-2986 System support for multi-service traffic Dixon, Michael J. University of Cambridge, Computer Laboratory 1992-01 en Text UCAM-CL-TR-245 ISSN 1476-2986 Digital network technology is now capable of supporting the bandwidth requirements of diverse applications such as voice, video and data (so called multi-service traffic). Some media, for example voice, have specific transmission requirements regarding the maximum packet delay and loss which they can tolerate. Problems arise when attempting to multiplex such traffic over a single channel. Traditional digital networks based on the Packet- (PTM) and Synchronous- (STM) Transfer Modes prove unsuitable due to their media access contention and inflexible bandwidth allocation properties respectively. The Asynchronous Transfer Mode (STM) has been proposed as a compromise between the PTM and STM techniques. The current state of multimedia research suggests that a significant amount of multi-service traffic will be handled by computer operating systems. Unfortunately conventional operating systems are largely unsuited to such a task. This dissertation is concerned with the system organisation necessary in order to extend the benefits of ATM networking through the endpoint operating system and up to the application level. A locally developed micro-kernel, with ATM network protocol support, has been used as a testbed for the ideas presented. Practical results over prototype ATM networks, including the 512 MHz Cambridge Backbone Network, are presented. A relevance-based utterance processing system Poznanski, Victor University of Cambridge, Computer Laboratory 1992-02 en Text UCAM-CL-TR-246 ISSN 1476-2986 Programming metalogics with a fixpoint type Crole, Roy Luis University of Cambridge, Computer Laboratory 1992-02 en Text UCAM-CL-TR-247 ISSN 1476-2986 On efficiency in theorem provers which fully expand proofs into primitive inferences Boulton, Richard J. University of Cambridge, Computer Laboratory 1992-02 en Text UCAM-CL-TR-248 ISSN 1476-2986 Theorem Provers which fully expand proofs into applications of primitive inference rules can be made highly secure, but have been criticized for being orders of magnitude slower than many other theorem provers. We argue that much of this relative inefficiency is due to the way proof procedures are typically written and not all is inherent in the way the systems work. We support this claim by considering a proof procedure for linear arithmetic. We show that straightforward techniques can be used to significantly cut down the computation required. An order of magnitude improvement in the performance is shown by an implementation of these techniques. A formalisation of the VHDL simulation cycle Van Tassel, John P. University of Cambridge, Computer Laboratory 1992-03 en Text UCAM-CL-TR-249 ISSN 1476-2986 The VHSIC Hardware Description Language (VHDL) has been gaining wide acceptance as a unifying HDL. It is, however, still a language in which the only way of validating a design is by careful simulation. With the aim of better understanding VHDL's particular simulation process and eventually reasoning about it, we have developed a formalisation of VHDL's simulation cycle for a subset of the language. It has also been possible to embed our semantics in the Cambridge Higher-Order Logic (HOL) system and derive interesting properties about specific VHDL programs. TouringMachines: autonomous agents with attitudes Ferguson, Innes A. University of Cambridge, Computer Laboratory 1992-04 en Text UCAM-CL-TR-250 ISSN 1476-2986 Multipoint digital video communication Jiang, Xiaofeng University of Cambridge, Computer Laboratory 1992-04 en Text UCAM-CL-TR-251 ISSN 1476-2986 A co-induction principle for recursively defined domains Pitts, Andrew M. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-252 ISSN 1476-2986 The (other) Cambridge ACQUILEX papers Sanfilippo, Antonio University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-253 ISSN 1476-2986 A HOL semantics for a subset of ELLA Boulton, Richard J. University of Cambridge, Computer Laboratory 1992-04 en Text UCAM-CL-TR-254 ISSN 1476-2986 Formal verification is an important tool in the design of computer systems, especially when the systems are safety or security critical. However, the formal techniques currently available are not well integrated into the set of tools more traditionally used by designers. This work is aimed at improving the integration by providing a formal semantics for a subset of the hardware description language ELLA, and by supporting this semantics in the HOL theorem proving system, which has been used extensively for hardware verification. A semantics for a subset of ELLA is described, and an outline of a proof of the equivalence of parallel and recursive implementations of an n-bit adder is given as an illustration of the semantics. The proof has been performed in an extension of the HOL system. Some proof tools written to support the verification are also described. The formal verification of hard real-time systems Cardell-Oliver, Rachel Mary University of Cambridge, Computer Laboratory 1992 en Text UCAM-CL-TR-255 ISSN 1476-2986 MCPL programming manual Richards, Martin University of Cambridge, Computer Laboratory 1992-05 en Text UCAM-CL-TR-256 ISSN 1476-2986 Cut-free sequent and tableau systems for propositional normal modal logics Goré, Rajeev Prakhakar University of Cambridge, Computer Laboratory 1992-05 en Text UCAM-CL-TR-257 ISSN 1476-2986 Private ATM networks Greaves, David J. McAuley, Derek University of Cambridge, Computer Laboratory 1992-05 en Text UCAM-CL-TR-258 ISSN 1476-2986 Full abstraction in the Lazy Lambda Calculus Abramsky, Samson Ong, C.-H. Luke University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-259 ISSN 1476-2986 Local computation of alternating fixed-points Anderson, Henrik Reif University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-260 ISSN 1476-2986 Image resampling Dodgson, Neil Anthony University of Cambridge, Computer Laboratory 1992-08 en Text UCAM-CL-TR-261 ISSN 1476-2986 Image resampling is the process of geometrically transforming digital images. This report considers several aspects of the process. We begin by decomposing the resampling process into three simpler sub-processes: reconstruction of a continuous intensity surface from a discrete image, transformation of that continuous surface, and sampling of the transformed surface to produce a new discrete image. We then consider the sampling process, and the subsidiary problem of intensity quantisation. Both these are well understood, and we present a summary of existing work, laying a foundation for the central body of the report where the sub-process of reconstruction is studied. The work on reconstruction divides into four parts, two general and two specific: 1. Piecewise local polynomials: the most studied group of reconstructors. We examine these, and the criteria used in their design. One new derivation is of two piecewise local quadratic reconstructors. 2. Infinite extent reconstructors: we consider these and their local approximations, the problem of finite image size, the resulting edge effects, and the solutions to these problems. Amongst the reconstructors discussed are the interpolating cubic B-spline and the interpolating Bezier cubic. We derive the filter kernels for both of these, and prove that they are the same. Given this kernel we demonstrate how the interpolating cubic B-spline can be extended from a one-dimensional to a two-dimensional reconstructor, providing a considerable speed improvement over the existing method of extension. 3. Fast Fourier transform reconstruction: it has long been known that the fast Fourier transform (FFT) can be used to generate an approximation to perfect scaling of a sample set. Donald Fraser (in 1987) took this result and generated a hybrid FFT reconstructor which can be used for general transformations, not just scaling. We modify Fraser’s method to tackle two major problems: its large time and storage requirements, and the edge effects it causes in the reconstructed intensity surface. 4. A priori knowledge reconstruction: first considering what can be done if we know how the original image was sampled, and then considering what can be done with one particular class of image coupled with one particular type of sampling. In this latter case we find that exact reconstruction of the image is possible. This is a surprising result as this class of images cannot be exactly reconstructed using classical sampling theory. The final section of the report draws all of the strands together to discuss transformations and the resampling process as a whole. Of particular note here is work on how the quality of different reconstruction and resampling methods can be assessed. Term assignment for intuitionistic linear logic (preliminary report) Benton, Nick Bierman, Gavin de Paiva, Valeria University of Cambridge, Computer Laboratory 1992-08 en Text UCAM-CL-TR-262 ISSN 1476-2986 The Lazy Lambda Calculus: an investigation into the foundations of functional programming Ong, C.-H. Luke University of Cambridge, Computer Laboratory 1992-08 en Text UCAM-CL-TR-263 ISSN 1476-2986 CCS with environmental guards Camilleri, Juanito University of Cambridge, Computer Laboratory 1992-08 en Text UCAM-CL-TR-264 ISSN 1476-2986 Reasoning with inductively defined relations in the HOL theorem prover Camilleri, Juanito Melham, Tom University of Cambridge, Computer Laboratory 1992-08 en Text UCAM-CL-TR-265 ISSN 1476-2986 Automatic exploitation of OR-parallelism in Prolog Klein, Carole University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-266 ISSN 1476-2986 Untyped strictness analysis Ernoult, Christine Mycroft, Alan University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-267 ISSN 1476-2986 Network file server design for continuous media Jardetzky, Paul W. University of Cambridge, Computer Laboratory 1992-10 en Text UCAM-CL-TR-268 ISSN 1476-2986 This dissertation concentrates on issues related to the provision of a network based storage facility for digital audio and video data. The goal is to demonstrate that a distributed file service in support of these media may be built without special purpose hardware. The main objective is to identify those parameters that affect file system performance and provide the criteria for making desirable design decisions. Optimising compilation Mycroft, Alan Norman, Arthur University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-269 ISSN 1476-2986 Designing a universal name service Ma, Chaoying University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-270 ISSN 1476-2986 Generally speaking, naming in computing systems deals with the creation of object identifiers at all levels of system architecture and the mapping among them. Two of the main purposes of having names in computer systems are (a) to identify objects; (b) to accomplish sharing. Without naming no computer system design can be done. The rapid development in the technology of personal workstations and computer communication networks has placed a great number of demands on designing large computer naming systems. In this dissertation, issues of naming in large distributed computing systems are addressed. Technical aspects as well as system architecture are examined. A design of a Universal Name Service (UNS) is proposed and its prototype implementation is described. Three major issues on designing a global naming system are studied. Firstly, it is observed that none of the existing name services provides enough flexibility in restructuring name spaces, more research has to be done. Secondly it is observed that although using stale naming data (hints) at the application level is acceptable in most cases as long as it is detectable and recoverable, stronger naming data integrity should be maintained to provide a better guarantee of finding objects, especially when a high degree of availability is required. Finally, configuring the name service is usually done in an ad hoc manner, leading to unexpected interruptions or a great deal of human intervention when the system is reconfigured. It is necessary to make a systematic study of automatic configuration and reconfiguration of name services. This research is based on a distributed computing model, in which a number of computers work cooperatively to provide the service. The contributions include: (a) the construction of a Globally Unique Directory Identifier (GUDI) name space. Flexible name space restructuring is supported by allowing directories to be added to or removed from the GUDI name space. (b) The definition of a two class name service infrastructure which exploits the semantics of naming. It makes the UNS replication control more robust, reliable as well as highly available. (c) The identification of two aspects in the name service configuration: one is concerned with the replication configuration, and the other is concerned with the server configuration. It is notable that previous work only studied these two aspects individually but not in combination. A distinguishing feature of the UNS is that both issues are considered at the design stage and novel methods are used to allow dynamic service configuration to be done automatically and safely. Set theory as a computational logic: I. from foundations to functions Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1992-11 en Text UCAM-CL-TR-271 ISSN 1476-2986 A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the flexibility to adapt to variants of set theory. Its higher-order syntax supports the definition of new binding operators. Unknowns in subgoals can be instantiated incrementally. The paper describes the derivation of rules for descriptions, relations and functions, and discusses interactive proofs of Cantor’s Theorem, the Composition of Homomorphisms challenge, and Ramsey’s Theorem. A generic proof assistant can stand up against provers dedicated to particular logics. Interactive program derivation Coen, Martin David University of Cambridge, Computer Laboratory 1992-11 en Text UCAM-CL-TR-272 ISSN 1476-2986 As computer programs are increasingly used in safety critical applications, program correctness is becoming more important; as the size and complexity of programs increases, the traditional approach of testing is becoming inadequate. Proving the correctness of programs written in imperative languages is awkward; functional programming languages, however, offer more hope. Their logical structure is cleaner, and it is practical to reason about terminating functional programs in an internal logic. This dissertation describes the development of a logical theory called TPT for reasoning about the correctness of terminating functional programs, its implementation using the theorem prover Isabelle, and its use in proving formal correctness. The theory draws both from Martin-Löf’s work in type theory and Manna and Waldinger’s work in program synthesis. It is based on classical first-order logic, and it contains terms that represent classes of behaviourally equivalent programs, types that denote sets of terminating programs and well-founded orderings. Well-founded induction is used to reason about general recursion in a natural way and to separate conditions for termination from those for correctness. The theory is implemented using the generic theorem prover Isabelle, which allows correctness proofs to be checked by machine and partially automated using tactics. In particular, tactics for type checking use the structure of programs to direct proofs. Type checking allows both the verification and derivation of programs, reducing specifications of correctness to sets of correctness conditions. These conditions can be proved in typed first-order logic, using well-known techniques of reasoning by induction and rewriting, and then lifted up to TPT. Examples of program termination are asserted and proved, using simple types. Behavioural specifications are expressed using dependent types, and the correctness of programs asserted and then proved. As a non-trivial example, a unification algorithm is specified and proved correct by machine. The work in this dissertation clearly shows how a classical theory can be used to reason about program correctness, how general recursion can be reasoned about, and how programs can direct proofs of correctness. TouringMachines: an architecture for dynamic, rational, mobile agents Ferguson, Innes A. University of Cambridge, Computer Laboratory 1992-11 en Text UCAM-CL-TR-273 ISSN 1476-2986 It is becoming widely accepted that neither purely reactive nor purely deliberative control techniques are capable of producing the range of behaviours required of intelligent computational or robotic agents in dynamic, unpredictable, multi-agent worlds. We present a new architecture for controlling autonomous, mobile agents – building on previous work addressing reactive and deliberative control methods. The proposed multi-layered control architecture allows a resource-bounded, goal-directed agent to react promptly to unexpected changes in its environment; at the same time it enables the agent to reason predictively about potential conflicts by constructing and projecting causal models or theories which hypothesise other agents’ goals and intentions. The line of research adopted is very much a pragmatic one. A single, common architecture has been implemented which, being extensively parametrized, allows an experimenter to study functionally- and behaviourally-diverse agent configurations. A principal aim of this research is to understand the role different functional capabilities play in constraining an agent’s behaviour under varying environmental conditions. To this end, we have constructed an experimental testbed comprising a simulated multi-agent world in which a variety of agent configurations and behaviours have been investigated. Experience with the new control architecture is described. Of what use is a verified compiler specification? Curzon, Paul University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-274 ISSN 1476-2986 Exploratory learning in the game of GO Pell, Barney University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-275 ISSN 1476-2986 This paper considers the importance of exploration to game-playing programs which learn by playing against opponents. The central question is whether a learning program should play the move which offers the best chance of winning the present game, or if it should play the move which has the best chance of providing useful information for future games. An approach to addressing this question is developed using probability theory, and then implemented in two different learning methods. Initial experiments in the game of Go suggest that a program which takes exploration into account can learn better against a knowledgeable opponent than a program which does not. METAGAME: a new challenge for games and learning Pell, Barney University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-276 ISSN 1476-2986 In most current approaches to Computer Game-Playing, including those employing some form of machine learning, the game analysis mainly is performed by humans. Thus, we are sidestepping largely the interesting (and difficult) questions. Human analysis also makes it difficult to evaluate the generality and applicability of different approaches. To address these problems, we introduce a new challenge: Metagame. The idea is to write programs which take as input the rules of a set of new games within a pre-specified class, generated by a program which is publicly available. The programs compete against each other in many matches on each new game, and they can then be evaluated based on their overall performance and improvement through experience. This paper discusses the goals, research areas, and general concerns for the idea of Metagame. METAGAME in symmetric chess-like games Pell, Barney University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-277 ISSN 1476-2986 I have implemented a game generator that generates games from a wide but still restricted class. This class is general enough to include most aspects of many standard games, including Chess, Shogi, Chinese Chess, Checkers, Draughts, and many variants of Fairy Chess. The generator, implemented in Prolog is transparent and publicly available, and generates games using probability distributions for parameters such as piece complexity, types of movement, board size, and locality. The generator is illustrated by means of a new game it produced, which is then subjected to a simple strategic analysis. This form of analysis suggests that programs to play Metagame well will either learn or apply very general game-playing principles. But because the class is still restricted, it may be possible to develop a naive but fast program which can outplay more sophisticated opponents. Performance in a tournament between programs is the deciding criterion. A formalization of the process algebra CCS in high order logic Nesi, Monica University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-278 ISSN 1476-2986 This paper describes a mechanization in higher order logic of the theory for a subset of Milner’s CCS. The aim is to build a sound and effective tool to support verification and reasoning about process algebra specifications. To achieve this goal, the formal theory for pure CCS (no value passing) is defined in the interactive theorem prover HOL, and a set of proof tools, based on the algebraic presentation of CCS, is provided. The transition assertions specification method Carreño, Victor A. University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-279 ISSN 1476-2986 Introduction to Isabelle Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1993-01 en Text UCAM-CL-TR-280 ISSN 1476-2986 Isabelle is a generic theorem prover, supporting formal proof in a variety of logics. Through a variety of examples, this paper explains the basic theory demonstrates the most important commands. It serves as the introduction to other Isabelle documentation. Pegasus project description Mullender, Sape J. Leslie, Ian M. McAuley, Derek University of Cambridge, Computer Laboratory 1992-09 en Text UCAM-CL-TR-281 ISSN 1476-2986 Pegasus – Operating system support for distributed multimedia systems Leslie, Ian M. McAuley, Derek Mullender, Sape J. University of Cambridge, Computer Laboratory 1992-12 en Text UCAM-CL-TR-282 ISSN 1476-2986 The Isabelle reference manual Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-283 ISSN 1476-2986 This manual is a comprehensive description of Isabelle, including all commands, functions and packages. It is intended for reference rather than for reading through, and is certainly not a tutorial. The manual assumes familiarity with the basic concepts explained in Introduction to Isabelle. Functions are organized by their purpose, by their operands (subgoals, tactics, theorems), and by their usefulness. In each section, basic functions appear first, then advanced functions, and finally esoteric functions. The Alvey Natural Language Tools grammar (4th Release) Grover, Claire Carroll, John Briscoe, Ted University of Cambridge, Computer Laboratory 1993-01 en Text UCAM-CL-TR-284 ISSN 1476-2986 Functional programming and input/output Gordon, Andrew Donald University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-285 ISSN 1476-2986 Isabelle’s object-logics Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-286 ISSN 1476-2986 Several logics come with Isabelle. Many of them are sufficiently developed to serve as comfortable reasoning environments. They are also good starting points for defining new logics. Each logic is distributed with sample proofs, some of which are presented in the paper. The logics described include first-order logic, Zermelo-Fraenkel set theory, higher-order logic, constructive type theory, and the classical sequent calculus LK. A final chapter explains the fine points of defining logics in Isabelle. A mechanised definition of Silage in HOL Gordon, Andrew D. University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-287 ISSN 1476-2986 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, by mapping Silage declarations into HOL predicates. The definition has been mechanised in the HOL theorem prover to support the transformational design of Silage circuits as theorem proving in HOL. Cut-free sequent and tableau systems for propositional Diodorean modal logics Gore, Rajeev University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-288 ISSN 1476-2986 The semantics of noun phrase anaphora Elworthy, David Alan Howard University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-289 ISSN 1476-2986 Discourse modelling for automatic summarising Spärck Jones, Karen University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-290 ISSN 1476-2986 Evaluating natural language processing systems Galliers, J.R. Spärck Jones, K. University of Cambridge, Computer Laboratory 1993-02 en Text UCAM-CL-TR-291 ISSN 1476-2986 This report presents a detailed analysis and review of NLP evaluation, in principle and in practice. Part 1 examines evaluation concepts and establishes a framework for NLP system evaluation. This makes use of experience in the related area of information retrieval and the analysis also refers to evaluation in speech processing. Part 2 surveys significant evaluation work done so far, for instance in machine translation, and discusses the particular problems of generic system evaluation. The conclusion is that evaluation strategies and techniques for NLP need much more development, in particular to take proper account of the influence of system tasks and settings. Part 3 develops a general approach to NLP evaluation, aimed at methodologically-sound strategies for test and evaluation motivated by comprehensive performance factor identification. The analysis throughout the report is supported by extensive illustrative examples. Synchronisation services for digital continuous media Sreenan, Cormac John University of Cambridge, Computer Laboratory 1993-03 en Text UCAM-CL-TR-292 ISSN 1476-2986 The development of broadband ATM networking makes it attractive to use computer communication networks for the transport of digital audio and motion video. Coupled with advances in workstation technology, this creates the opportunity to integrate these continuous information media within a distributed computing system. Continuous media have an inherent temporal dimension, resulting in a set of synchronisation requirements which have real-time constraints. This dissertation identifies the role and position of synchronisation, in terms of the support which is necessary in an integrated distributed system. This work is supported by a set of experiments which were performed in an ATM inter-network using multi-media workstations, each equipped with an Olivetti Pandora Box. Objects and transactions for modelling distributed applications: concurrency control and commitment Bacon, Jean Moody, Ken University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-293 ISSN 1476-2986 OPERA : Storage, programming and display of multimedia objects Moody, Ken Bacon, Jean Adly, Noha Afshar, Mohamad Bates, John Feng, Huang Hayton, Richard Lo, Sai Lai Schwiderski, Scarlet Sultana, Robert Wu, Zhixue University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-294 ISSN 1476-2986 OPERA : Storage and presentation support for multimedia applications in a distributed, ATM network environment Bacon, Jean Bates, John Lo, Sai Lai Moody, Ken University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-295 ISSN 1476-2986 A persistent programming language for multimedia databases in the OPERA project Wu, Z. Moody, K. Bacon, J. University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-296 ISSN 1476-2986 Categorical abstract machines for higher-order lambda calculi Ritter, Eike University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-297 ISSN 1476-2986 Multicast in the asynchronous transfer mode environment Doar, John Matthew Simon University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-298 ISSN 1476-2986 In future multimedia communication networks, the ability to multicast information will be useful for many new and existing services. This dissertation considers the design of multicast switches for Asynchronous Transfer Mode (ATM) networks and proposes one design based upon a slotted ring. Analysis and simulation studies of this design are presented and details of its implementation for an experimental ATM network (Project Fairisle) are described, together with the modifications to the existing multi-service protocol architecture necessary to provide multicast connections. Finally, a short study of the problem of multicast routing is presented, together with some simulations of the long-term effect upon the routing efficiency of modifying the number of destinations within a multicast group. Pragmatic reasoning in bridge Gamback, Bjorn Rayner, Manny Pell, Barney University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-299 ISSN 1476-2986 In this paper we argue that bidding in the game of Contract Bridge can profitably be regarded as a micro-world suitable for experimenting with pragmatics. We sketch an analysis in which a “bidding system” is treated as the semantics of an artificial language, and show how this “language”, despite its apparent simplicity, is capable of supporting a wide variety of common speech acts parallel to those in natural languages; we also argue that the reason for the relatively unsuccessful nature of previous attempts to write strong Bridge playing programs has been their failure to address the need to reason explicitly about knowledge, pragmatics, probabilities and plans. We give an overview of Pragma, a system currently under development, which embodies these ideas in concrete form, using a combination of rule-based inference, stochastic simulation, and “neural-net” learning. Examples are given illustrating the functionality of the system in its current form. Formal verification of VIPER’s ALU Wong, Wai University of Cambridge, Computer Laboratory 1993-04 en Text UCAM-CL-TR-300 ISSN 1476-2986 The dual-level validation concurrency control method Wu, Zhixue Moody, Ken Bacon, Jean University of Cambridge, Computer Laboratory 1993-06 en Text UCAM-CL-TR-301 ISSN 1476-2986 Logic programming for general game-playing Pell, Barney University of Cambridge, Computer Laboratory 1993-06 en Text UCAM-CL-TR-302 ISSN 1476-2986 Meta-Game Playing is a new approach to games in Artificial Intelligence, where we construct programs to play new games in a well-defined class, which are output by an automatic game generator. As the specific games to be played are not known in advance, a degree of human bias is eliminated, and playing programs are required to perform any game-specific optimisations without human assistance. The attempt to construct a general game-playing program is made difficult by the opposing goals of generality and efficiency. This paper shows how application of standard techniques in logic-programming (abstract interpretation and partial evaluation) makes it possible to achieve both of these goals. Using these techniques, we can represent the semantics of a large class of games in a general and declarative way, but then have the program transform this representation into a more efficient version once it is presented with the rules of a new game. This process can be viewed as moving some of the responsibility for game analysis (that concerned with efficiency) from the researcher to the program itself. Drawing trees — a case study in functional programming Kennedy, Andrew University of Cambridge, Computer Laboratory 1993-06 en Text UCAM-CL-TR-303 ISSN 1476-2986 Co-induction and co-recursion in higher-order logic Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1993-07 en Text UCAM-CL-TR-304 ISSN 1476-2986 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 and verification. It supports reasoning about a wide range of computable functions, but it does not formalize their operational semantics and can express noncomputable functions also. The theory is demonstrated using lists and lazy lists as examples. The emphasis is on using co-recursion to define lazy list functions, and on using co-induction to reason about them. Strong normalisation for the linear term calculus Benton, P.N. University of Cambridge, Computer Laboratory 1993-07 en Text UCAM-CL-TR-305 ISSN 1476-2986 Recording HOL proofs Wong, Wai University of Cambridge, Computer Laboratory 1993-07 en Text UCAM-CL-TR-306 ISSN 1476-2986 Natural language processing for information retrieval Lewis, David D. Spärck Jones, Karen University of Cambridge, Computer Laboratory 1993-07 en Text UCAM-CL-TR-307 ISSN 1476-2986 The paper summarizes the essential properties of document retrieval and reviews both conventional practice and research findings, the latter suggesting that simple statistical techniques can be effective. It then considers the new opportunities and challenges presented by the ability to search full text directly (rather than e.g. titles and abstracts), and suggests appropriate approaches to doing this, with a focus on the role of natural language processing. The paper also comments on possible connections with data and knowledge retrieval, and concludes by emphasizing the importance of rigorous performance testing. A case study of co-induction in Isabelle HOL Frost, Jacob University of Cambridge, Computer Laboratory 1993-08 en Text UCAM-CL-TR-308 ISSN 1476-2986 The consistency of the dynamic and static semantics for a small functional programming language was informally proved by R. Milner and M. Tofte. The notions of co-inductive definitions and the associated principle of co-induction played a pivotal role in the proof. With emphasis on co-induction, the work presented here deals with the formalisation of this result in the higher-order logic of the generic theorem prover Isabelle. Strictness analysis of lazy functional programs Benton, Peter Nicholas University of Cambridge, Computer Laboratory 1993-08 en Text UCAM-CL-TR-309 ISSN 1476-2986 HARP: a hierarchical asynchronous replication protocol for massively replicated systems Adly, Noha University of Cambridge, Computer Laboratory 1993-08 en Text UCAM-CL-TR-310 ISSN 1476-2986 A verified Vista implementation Curzon, Paul University of Cambridge, Computer Laboratory 1993-09 en Text UCAM-CL-TR-311 ISSN 1476-2986 Set theory for verification: II : Induction and recursion Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1993-09 en Text UCAM-CL-TR-312 ISSN 1476-2986 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 to a set that is closed under Cartesian product and disjoint sum. Worked examples include the transitive closure of a relation, lists, variable-branching trees and mutually recursive trees and forests. The Schröder-Bernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions. Proof by pointing Bertot, Yves Kahn, Gilles Théry, Laurent University of Cambridge, Computer Laboratory 1993-10 en Text UCAM-CL-TR-313 ISSN 1476-2986 Practical unification-based parsing of natural language Carroll, John Andrew University of Cambridge, Computer Laboratory en Text UCAM-CL-TR-314 ISSN 1476-2986 The thesis describes novel techniques and algorithms for the practical parsing of realistic Natural Language (NL) texts with a wide-coverage unification-based grammar of English. The thesis tackles two of the major problems in this area: firstly, the fact that parsing realistic inputs with such grammars can be computationally very expensive, and secondly, the observation that many analyses are often assigned to an input, only one of which usually forms the basis of the correct interpretation. The thesis starts by presenting a new unification algorithm, justifies why it is well-suited to practical NL parsing, and describes a bottom-up active chart parser which employs this unification algorithm together with several other novel processing and optimisation techniques. Empirical results demonstrate that an implementation of this parser has significantly better practical performance than a comparable, state-of-the-art unification-based parser. Next, techniques for computing an LR table for a large unification grammar are described, a context free non-deterministic LR parsing algorithm is presented which has better time complexity than any previously reported using the same approach, and a unification-based version is derived. In experiments, the performance of an implementation of the latter is shown to exceed both the chart parser and also that of another efficient LR-like algorithm recently proposed. Building on these methods, a system for parsing text taken from a given corpus is described which uses probabilistic techniques to identify the most plausible syntactic analyses for an input from the often large number licensed by the grammar. New techniques implemented include an incremental approach to semi-supervised training, a context-sensitive method of scoring sub-analyses, the accurate manipulation of probabilities during parsing, and the identification of the highest ranked analyses without exhaustive search. The system attains a similar success rate to approaches based on context-free grammar, but produces analyses which are more suitable for semantic processing. The thesis includes detailed analyses of the worst-case space and time complexities of all the main algorithms described, and discusses the practical impact of the theoretical complexity results. Strategy generation and evaluation for meta-game playing Pell, Barney Darryl University of Cambridge, Computer Laboratory 1993-11 en Text UCAM-CL-TR-315 ISSN 1476-2986 Meta-Game Playing (METAGAME) is a new paradigm for research in game-playing in which we design programs to take in the rules of unknown games and play those games without human assistance. Strong performance in this new paradigm is evidence that the program, instead of its human designer, has performed the analysis of each specific game. SCL-METAGAME is a concrete METAGAME research problem based around the class of symmetric chess-like games. The class includes the games of chess, checkers, noughts and crosses, Chinese-chess, and Shogi. An implemented game generator produces new games in this class, some of which are objects of interest in their own right. METAGAMER is a program that plays SCL-METAGAME. The program takes as input the rules of a specific game and analyses those rules to construct for that game an efficient representation and an evaluation function, both for use with a generic search engine. The strategic analysis performed by the program relates a set of general knowledge sources to the details of the particular game. Among other properties, this analysis determines the relative value of the different pieces in a given game. Although METAGAMER does not learn from experience, the values resulting from its analysis are qualitatively similar to values used by experts on known games, and are sufficient to produce competitive performance the first time the program actually plays each game it is given. This appears to be the first program to have derived useful piece values directly from analysis of the rules of different games. Experiments show that the knowledge implemented in METAGAMER is useful on games unknown to its programmer in advance of the competition and make it seem likely that future programs which incorporate learning and more sophisticated active-analysis techniques will have a demonstrable competitive advantage on this new problem. When playing the known games of chess and checkers against humans and specialised programs, METAGAMER has derived from more general principles some strategies which are familiar to players of those games and which are hard-wired in many game-specific programs. The Compleat LKB Copestake, Ann University of Cambridge, Computer Laboratory 1993-08 en Text UCAM-CL-TR-316 ISSN 1476-2986 Femto-VHDL: the semantics of a subset of VHDL and its embedding in the HOL proof assistant Van Tassel, John Peter University of Cambridge, Computer Laboratory 1993-11 en Text UCAM-CL-TR-317 ISSN 1476-2986 A method of program refinement Grundy, Jim University of Cambridge, Computer Laboratory 1993-11 en Text UCAM-CL-TR-318 ISSN 1476-2986 A method of specifying the desired behaviour of a computer program, and of refining such specifications into imperative programs is proposed. The refinement method has been designed with the intention of being amenable to tool support, and of being applicable to real-world refinement problems. Part of the refinement method proposed involves the use of a style of transformational reasoning called ‘window inference’. Window inference is particularly powerful because it allows the information inherent in the context of a subexpression to be used in its transformation. If the notion of transformational reasoning is generalised to include transformations that preserve relationships weaker than equality, then program refinement can be regarded as a special case of transformational reasoning. A generalisation of window inference is described that allows non-equivalence preserving transformations. Window inference was originally proposed independently from, and as an alternative to, traditional styles of reasoning. A correspondence between the generalised version of window inference and natural deduction is described. This correspondence forms the basis of a window inference tool that has been built on top of the HOL theorem proving system. This dissertation adopts a uniform treatment of specifications and programs as predicates. A survey of the existing approaches to the treatment of programs as predicates is presented. A new approach is then developed based on using predicates of a three-valued logic. This new approach can distinguish more easily between specifications of terminating and nonterminating behaviour than can the existing approaches. A method of program refinement is then described by combining the unified treatment of specifications and programs as three-valued predicates with the window inference style of transformational reasoning. The result is a simple method of refinement that is well suited to the provision of tool support. The method of refinement includes a technique for developing recursive programs. The proof of such developments is usually complicated because little can be assumed about the form and termination properties of a partially developed program. These difficulties are side-stepped by using a simplified meaning for recursion that compels the development of terminating programs. Once the development of a program is complete, the simplified meaning for recursion is refined into the true meaning. The dissertation concludes with a case study which presents the specification and development of a simple line-editor. The case study demonstrates the applicability of the refinement method to real-world problems. The line editor is a nontrivial example that contains features characteristic of large developments, including complex data structures and the use of data abstraction. Examination of the case study shows that window inference offers a convenient way of structuring large developments. A workstation architecture to support multimedia Hayter, Mark David University of Cambridge, Computer Laboratory 1993-11 en Text UCAM-CL-TR-319 ISSN 1476-2986 The advent of high speed networks in the wide and local area enables multimedia traffic to be easily carried between workstation class machines. The dissertation considers an architecture for a workstation to support such traffic effectively. In addition to presenting the information to a human user the architecture allows processing to be done on continuous media streams. The proposed workstation architecture, known as the Desk Area Network (DAN), extends ideas from Asynchronous Transfer Mode (ATM) networks into the end-system. All processors and devices are connected to an ATM interconnect. The architecture is shown to be capable of supporting both multimedia data streams and more traditional CPU cache line traffic. The advocated extension of the CPU cache which allows caching of multimedia data streams is shown to provide a natural programming abstraction and a mechanism for synchronising the processor with the stream. A prototype DAN workstation has been built. Experiments have been done to demonstrate the features of the architecture. In particular the use of the DAN as a processor-to-memory interconnect is closely studied to show the practicality of using ATM for cache line traffic in a real machine. Simple demonstrations of the stream cache ideas are used to show its utility in future applications. A fixedpoint approach to implementing (co)inductive definitions (updated version) Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-320 ISSN 1476-2986 Several theorem provers provide commands for formalizing recursive datatypes or inductively defined sets. This paper presents a new approach, based on fixedpoint definitions. It is unusually general: it admits all monotone inductive definitions. It is conceptually simple, which has allowed the easy implementation of mutual recursion and other conveniences. It also handles coinductive definitions: simply replace the least fixedpoint by a greatest fixedpoint. This represents the first automated support for coinductive definitions. The method has been implemented in Isabelle’s formalization of ZF set theory. It should be applicable to any logic in which the Knaster-Tarski Theorem can be proved. The paper briefly describes a method of formalizing non-well-founded data structures in standard ZF set theory. Examples include lists of n elements, the accessible part of a relation and the set of primitive recursive functions. One example of a coinductive definition is bisimulations for lazy lists. Recursive datatypes are examined in detail, as well as one example of a “codatatype”: lazy lists. The appendices are simple user’s manuals for this Isabelle/ZF package. Relational properties of domains Pitts, Andrew M. University of Cambridge, Computer Laboratory 1993-12 en Text UCAM-CL-TR-321 ISSN 1476-2986 New tools are presented for reasoning about properties of recursively defined domains. We work within a general, category-theoretic framework for various notions of ‘relation’ on domains and for actions of domain constructors on relations. Freyd’s analysis of recursive types in terms of a property of mixed initiality/finality is transferred to a corresponding property of invariant relations. The existence of invariant relations is proved under completeness assumptions about the notion of relation. We show how this leads to simpler proofs of the computational adequacy of denotational semantics for functional programming languages with user-declared datatypes. We show how the initiality/finality property of invariant relations can be specialized to yield an induction principle for admissible subsets of recursively defined domains, generalizing the principle of structural induction for inductively defined sets. We also show how the initiality/finality property gives rise to the co-induction principle studied by the author (in UCAM-CL-TR-252), by which equalities between elements of recursively defined domains may be proved via an appropriate notion of ‘bisimulation’. Supporting distributed realtime computing Li, Guangxing University of Cambridge, Computer Laboratory 1993-12 en Text UCAM-CL-TR-322 ISSN 1476-2986 Representing higher-order logic proofs in HOL von Wright, J. University of Cambridge, Computer Laboratory 1994-01 en Text UCAM-CL-TR-323 ISSN 1476-2986 Verifying modular programs in HOL von Wright, J. University of Cambridge, Computer Laboratory 1994-01 en Text UCAM-CL-TR-324 ISSN 1476-2986 The temporal properties of English conditionals and modals Crouch, Richard University of Cambridge, Computer Laboratory 1994-01 en Text UCAM-CL-TR-325 ISSN 1476-2986 This thesis deals with the patterns of temporal reference exhibited by conditional and modal sentences in English, and specifically with the way that past and present tenses can undergo deictic shift in these contexts. This shifting behaviour has consequences both for the semantics of tense and for the semantics of conditionals and modality. Asymmetries in the behaviour of the past and present tenses under deictic shift are explained by positing a primary and secondary deictic centre for tenses. The two deictic centres, the assertion time and the verification time, are given independent motivation through an information based view of tense. This holds that the tense system not only serves to describe the way that the world changes over time, but also the way that information about the world changes. Information change takes place in two stages. First, it is asserted that some fact holds. And then, either at the same time or later, it is verified that is assertion is correct. Typically, assertion and verification occur simultaneously, and most sentences convey verified information. Modals and conditionals allow delayed assertion and verification. “If A, then B” means roughly: suppose you were now to assert A; if and when A is verified, you will be in a position to assert B, and in due course this assertion will also be verified. Since A and B will both be tensed clauses, the shifting of the primary and secondary deictic centres leads to shifted interpretations of the two clauses. The thesis presents a range of temporal properties of indicative and subjunctive conditionals that have not previously been discussed, and shows how they can be explained. A logic is presented for indicative conditionals, based around an extension of intuitionistic logic to allow for both verified and unverified assertions. This logic naturally gives rise to three forms of epistemic modality, corresponding to “must”, “may” and “will”. A modular and extensible network storage architecture Lo, Sai-Lai University of Cambridge, Computer Laboratory 1994-01 en Text UCAM-CL-TR-326 ISSN 1476-2986 Most contemporary distributed file systems are not designed to be extensible. This work asserts that the lack of extensibility is a problem because: – New data types, such as continuous-medium data and structured data, are significantly different from conventional unstructured data, such as text and binary, that contemporary distributed file systems are built to support. – Value-adding clients can provide functional enhancements, such as convenient and reliable persistent programming and automatic and transparent file indexing, but cannot be integrated smoothly with contemporary distributed file systems. – New media technologies, such as the optical jukebox and RAID disk, can extend the scale and performance of a storage service but contemporary distributed file systems do not have a clear framework to incorporate these new technologies and to provide the necessary user level transparency. Motivated by these observations, the new network storage architecture (MSSA) presented in this dissertation, is designed to be extensible. Design modularity is taken as the key to achieve service extensibility. This dissertation examines a number of issues related to the design of the architecture. New ideas, such as a flexible access control mechanism based on temporary capabilities, a low level storage substrate that uses non-volatile memory to provide atomic update semantics at high performance, a concept of sessions to differentiate performance requirements of different data types, are introduced. Prototype implementations of the key components are evaluated. A new application for explanation-based generalisation within automated deduction Baker, Siani L. University of Cambridge, Computer Laboratory 1994-02 en Text UCAM-CL-TR-327 ISSN 1476-2986 The formal verification of the Fairisle ATM switching element: an overview Curzon, Paul University of Cambridge, Computer Laboratory 1994-03 en Text UCAM-CL-TR-328 ISSN 1476-2986 The formal verification of the Fairisle ATM switching element Curzon, Paul University of Cambridge, Computer Laboratory 1994-03 en Text UCAM-CL-TR-329 ISSN 1476-2986 Interacting with paper on the DigitalDesk Wellner, Pierre David University of Cambridge, Computer Laboratory 1994-03 en Text UCAM-CL-TR-330 ISSN 1476-2986 In the 1970’s Xerox PARC developed the “desktop metaphor,” which made computers easy to use by making them look and act like ordinary desks and paper. This led visionaries to predict the “paperless office” would dominate within a few years, but the trouble with this prediction is that people like paper too much. It is portable, tactile, universally accepted, and easier to read than a screen. Today, we continue to use paper, and computers produce more of it than they replace. Instead of trying to use computers to replace paper, the DigitalDesk takes the opposite approach. It keeps the paper, but uses computers to make it more powerful. It provides a Computer Augmented Environment for paper. The DigitalDesk is built around an ordinary physical desk and can be used as such, but it has extra capabilities. A video camera is mounted above the desk, pointing down at the work surface. This camera’s output is fed through a system that can detect where the user is pointing, and it can read documents that are placed on the desk. A computer-driven electronic projector is also mounted above the desk, allowing the system to project electronic objects onto the work surface and onto real paper documents — something that can’t be done with flat display panels or rear-projection. The system is called DigitalDesk because it allows pointing with the fingers. Several applications have been prototyped on the DigitalDesk. The first was a calculator where a sheet of paper such as an annual report can be placed on the desk allowing the user to point at numbers with a finger or pen. The camera reads the numbers off the paper, recognizes them, and enters them into the display for further calculations. Another is a translation system which allows users to point at unfamiliar French words to get their English definitions projected down next to the paper. A third is a paper-based paint program (PaperPaint) that allows users to sketch on paper using traditional tools, but also be able to select and paste these sketches with the camera and projector to create merged paper and electronic documents. A fourth application is the DoubleDigitalDesk, which allows remote colleagues to “share” their desks, look at each other’s paper documents and sketch on them remotely. This dissertation introduces the concept of Computer Augmented Environments, describes the DigitalDesk and applications for it, and discusses some of the key implementation issues that need to be addressed to make this system work. It describes a toolkit for building DigitalDesk applications, and it concludes with some more ideas for future work. HPP: a hierarchical propagation protocol for large scale replication in wide area networks Adly, Noha Kumar, Akhil University of Cambridge, Computer Laboratory 1994-03 en Text UCAM-CL-TR-331 ISSN 1476-2986 Distributed computing with objects Evers, David Martin University of Cambridge, Computer Laboratory 1994-03 en Text UCAM-CL-TR-332 ISSN 1476-2986 What is a categorical model of intuitionistic linear logic? Bierman, G.M. University of Cambridge, Computer Laboratory 1994-04 en Text UCAM-CL-TR-333 ISSN 1476-2986 A concrete final coalgebra theorem for ZF set theory Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1994-05 en Text UCAM-CL-TR-334 ISSN 1476-2986 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 be modelled only using the variant tuples and functions. But the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint. The theory is intended for machine implementation and a simple case of it is already implemented using the theorem prover Isabelle. Video mail retrieval using voice: report on keyword definition and data collection (deliverable report on VMR task No. 1) Jones, G.J.F. Foote, J.T. Spärck Jones, K. Young, S.J. University of Cambridge, Computer Laboratory 1994-04 en Text UCAM-CL-TR-335 ISSN 1476-2986 This report describes the rationale, design, collection and basic statistics of the initial training and test database for the Cambridge Video Mail Retrieval (VMR) project. This database is intended to support both training for the wordspotting processes and testing for the document searching methods using these that are being developed for the project’s message retrieval task. Towards a proof theory of rewriting: the simply-typed 2-λ calculus Hilken, Barnaby P. University of Cambridge, Computer Laboratory 1994-05 en Text UCAM-CL-TR-336 ISSN 1476-2986 Efficiency in a fully-expansive theorem prover Boulton, Richard John University of Cambridge, Computer Laboratory 1994-05 en Text UCAM-CL-TR-337 ISSN 1476-2986 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 this purpose. The disadvantage with the approach is that performance is compromised. This is partly due to the inherent cost of fully expanding a proof but, as demonstrated in this thesis, much of the observed inefficiency is due to the way the derived proof procedures are written. This thesis seeks to identify sources of non-inherent inefficiency in the HOL system and proposes some general-purpose and some specialised techniques for eliminating it. One area that seems to be particularly amenable to optimisation is equational reasoning. This is significant because equational reasoning constitutes large portions of many proofs. A number of techniques are proposed that transparently optimise equational reasoning. Existing programs in the HOL system require little or no modification to work faster. The other major contribution of this thesis is a framework in which part of the computation involved in HOL proofs can be postponed. This enables users to make better use of their time. The technique exploits a form of lazy evaluation. The critical feature is the separation of the code that generates the structure of a theorem from the code that justifies it logically. Delaying the justification allows some non-local optimisations to be performed in equational reasoning. None of the techniques sacrifice the security of the fully-expansive approach. A decision procedure for a subset of the theory of linear arithmetic is used to illustrate many of the techniques. Decision procedures for this theory are commonplace in theorem provers due to the importance of arithmetic reasoning. The techniques described in the thesis have been implemented and execution times are given. The implementation of the arithmetic procedure is a major contribution in itself. For the first time, users of the HOL system are able to prove many arithmetic lemmas automatically in a practical amount of time (typically a second or two). The applicability of the techniques to other fully-expansive theorem provers and possible extensions of the ideas are considered. A new approach to implementing atomic data types Wu, Zhixue University of Cambridge, Computer Laboratory 1994-05 en Text UCAM-CL-TR-338 ISSN 1476-2986 Belief revision and dialogue management in information retrieval Logan, Brian Reece, Steven Cawsey, Alison Galliers, Julia Spärck Jones, Karen University of Cambridge, Computer Laboratory 1994-05 en Text UCAM-CL-TR-339 ISSN 1476-2986 This report describes research to evaluate a theory of belief revision proposed by Galliers in the context of information-seeking interaction as modelled by Belkin, Brooks and Daniels and illustrated by user-librarian dialogues. The work covered the detailed assessment and development, and computational implementation and testing, of both the belief revision theory and the information retrieval model. Some features of the belief theory presented problems, and the original ‘multiple expert’ retrieval model had to be drastically modified to support rational dialogue management. But the experimental results showed that the characteristics of literature seeking interaction could be successfully captured by the belief theory, exploiting important elements of the retrieval model. Thus, though the system’s knowledge and dialogue performance were very limited, it provides a useful base for further research. The report presents all aspects of the research in detail, with particular emphasis on the implementation of belief and intention revision, and the integration of revision with domain reasoning and dialogue interaction. Operating system support for quality of service Hyden, Eoin Andrew University of Cambridge, Computer Laboratory 1994-06 en Text UCAM-CL-TR-340 ISSN 1476-2986 The deployment of high speed, multiservice networks within the local area has meant that it has become possible to deliver continuous media data to a general purpose workstation. This, in conjunction with the increasing speed of modern microprocessors, means that it is now possible to write application programs which manipulate continuous media in real-time. Unfortunately, current operating systems do not provide the resource management facilities which are required to ensure the timely execution of such applications. This dissertation presents a flexible resource management paradigm, based on the notion of Quality of Service, with which it is possible to provide the scheduling support required by continuous media applications. The mechanisms which are required within an operating system to support this paradigm are described, and the design and implementation of a prototypical kernel which implements them is presented. It is shown that, by augmenting the interface between an application and the operating system, the application can be informed of varying resource availabilities, and can make use of this information to vary the quality of its results. In particular an example decoder application is presented, which makes use of such information and exploits some of the fundamental properties of continuous media data to trade video image quality for the amount of processor time which it receives. Presentation support for distributed multimedia applications Bates, John University of Cambridge, Computer Laboratory 1994-06 en Text UCAM-CL-TR-341 ISSN 1476-2986 An architecture for distributed user interfaces Freeman, Stephen Martin Guy University of Cambridge, Computer Laboratory 1994-07 en Text UCAM-CL-TR-342 ISSN 1476-2986 The contour tree image encoding technique and file format Turner, Martin John University of Cambridge, Computer Laboratory 1994-07 en Text UCAM-CL-TR-344 ISSN 1476-2986 A proof environment for arithmetic with the Omega rule Baker, Siani L. University of Cambridge, Computer Laboratory 1994-08 en Text UCAM-CL-TR-345 ISSN 1476-2986 On intuitionistic linear logic Bierman, G.M. University of Cambridge, Computer Laboratory 1994-08 en Text UCAM-CL-TR-346 ISSN 1476-2986 In this thesis we carry out a detailed study of the (propositional) intuitionistic fragment of Girard’s linear logic (ILL). Firstly we give sequent calculus, natural deduction and axiomatic formulations of ILL. In particular our natural deduction is different from others and has important properties, such as closure under substitution, which others lack. We also study the process of reduction in all three local formulations, including a detailed proof of cut elimination. Finally, we consider translations between Instuitionistic Logic (IL) and ILL. We then consider the linear term calculus, which arises from applying the Curry-Howard correspondence to the natural deduction formulation. We show how the various proof theoretic formulations suggest reductions at the level of terms. The properties of strong normalization and confluence are proved for these reduction rules. We also consider mappings between the extended λ-calculus and the linear term calculus. Next we consider a categorical model for ILL. We show how by considering the linear term calculus as an equational logic, we can derive a model: a linear category. We consider two alternative models: firstly, one due to Seely and then one due to Lafont. Surprisingly, we find that Seely’s model is not sound, in that equal terms are not modelled with equal morphisms. We show how after adapting Seely’s model (by viewing it in a more abstract setting) it becomes a particular instance of a linear category. We show how Lafont’s model can also be seen as another particular instance of a linear category. Finally we consider various categories of coalgebras, whose construction can be seen as a categorical equivalent of the translation of IL into ILL. Reflections on TREC Spärck Jones, Karen University of Cambridge, Computer Laboratory 1994-07 en Text UCAM-CL-TR-347 ISSN 1476-2986 This paper discusses the Text REtrieval Conferences (TREC) programme as a major enterprise in information retrieval research. It reviews its structure as an evaluation exercise, characterises the methods of indexing and retrieval being tested within it in terms of the approaches to system performance factors these represent; analyses the test results for solid, overall conclusions that can be drawn from them; and, in the light of the particular features of the test data, assesses TREC both for generally-applicable findings that emerge from it and for directions it offers for future research. Integrated sound synchronisation for computer animation Hunter, Jane Louise University of Cambridge, Computer Laboratory 1994-08 en Text UCAM-CL-TR-348 ISSN 1476-2986 A HOL interpretation of Noden Graham, Brian University of Cambridge, Computer Laboratory 1994-09 en Text UCAM-CL-TR-349 ISSN 1476-2986 Ten commandments of formal methods Bowen, Jonathan P. Hinchey, Michael G. University of Cambridge, Computer Laboratory 1994-09 en Text UCAM-CL-TR-350 ISSN 1476-2986 Handling realtime traffic in mobile networks Biswas, Subir Kumar University of Cambridge, Computer Laboratory 1994-09 en Text UCAM-CL-TR-351 ISSN 1476-2986 The rapidly advancing technology of cellular communication and wireless LAN makes ubiquitous computing feasible where the mobile users can have access to the location independent information and the computing resources. Multimedia networking is another emerging technological trend of the 1990s and there is an increasing demand for supporting continuous media traffic in wireless personal communication environment. In order to guarantee the strict performance requirements of realtime traffic, the connection-oriented approaches are proving to be more efficient compared to the conventional datagram based networking. This dissertation deals with a network architecture and its design issues for implementing the connection-oriented services in a mobile radio environment. The wired backbone of the proposed wireless LAN comprises of high speed ATM switching elements, connected in a modular fashion, where the new switches and the user devices can be dynamically added and reconnected for maintaining a desired topology. A dynamic reconfiguration protocol, which can cope with these changing network topologies, is proposed for the present network architecture. The details about a prototype implementation of the protocol and a simulation model for its performance evaluation are presented. CSMA/AED, a single frequency and carrier sensing based protocol is proposed for the radio medium access operations. A simulation model is developed in order to investigate the feasibility of this statistical and reliable access scheme for the proposed radio network architecture. The effectiveness of a per-connection window based flow control mechanism, for the proposed radio LAN, is also investigated. A hybrid technique is used, where the medium access and the radio data-link layers are modelled using the mentioned simulator; an upper layer end-to-end queueing model, involving flow dependent servers, is solved using an approximate Mean Value Analysis technique which is augmented for faster iterative convergence. A distributed location server, for managing mobile users’ location information and for aiding the mobile connection management tasks, is proposed. In order to hide the effects of mobility from the non-mobile network entities, the concept of a per-mobile software entity, known as a “representative”, is introduced. A mobile connection management scheme is also proposed for handling the end-to-end network layer connections in the present mobile environment. The scheme uses the representatives and a novel connection caching technique for providing the necessary realtime traffic support functionalities. A prototype system, comprising of the proposed location and the connection managers, has been built for demonstrating the feasibility of the presented architecture for transporting continuous media traffic. A set of experiments have been carried out in order to investigate the impacts of various design decisions and to identify the performance-critical parts of the design. A mixed linear and non-linear logic: proofs, terms and models Benton, P.N. University of Cambridge, Computer Laboratory 1994-10 en Text UCAM-CL-TR-352 ISSN 1476-2986 Merging HOL with set theory Gordon, Mike University of Cambridge, Computer Laboratory 1994-11 en Text UCAM-CL-TR-353 ISSN 1476-2986 Set theory is the standard foundation for mathematics, but the majority of general purpose mechanized proof assistants support versions of type theory (higher order logic). Examples include Alf, Automath, Coq, Ehdm, HOL, IMPS, Lambda, LEGO, Nuprl, PVS and Veritas. For many applications type theory works well and provides for specification the benefits of type-checking that are well known in programming. However, there are areas where types get in the way or seem unmotivated. Furthermore, most people with a scientific or engineering background already know set theory, whereas type theory may appear inaccessible and so be an obstacle to the uptake of proof assistants based on it. This paper describes some experiments (using HOL) in combining set theory and type theory; the aim is to get the best of both worlds in a single system. Three approaches have been tried, all based on an axiomatically specified type V of ZF-like sets: (i) HOL is used without any additions besides V; (ii) an embedding of the HOL logic into V is provided; (iii) HOL axiomatic theories are automatically translated into set-theoretic definitional theories. These approaches are illustrated with two examples: the construction of lists and a simple lemma in group theory. Formalising a model of the λ-calculus in HOL-ST Agerholm, Sten University of Cambridge, Computer Laboratory 1994-10 en Text UCAM-CL-TR-354 ISSN 1476-2986 Two cryptographic notes Wheeler, David Needham, Roger University of Cambridge, Computer Laboratory 1994-11 en Text UCAM-CL-TR-355 ISSN 1476-2986 A large block DES-like algorithm DES was designed to be slow in software. We give here a DES type of code which applies directly to single blocks comprising two or more words of 32 bits. It is thought to be at least as secure as performing DES separately on two word blocks, and has the added advantage of not requiring chaining etc. It is about 8m/(12+2m) times as fast as DES for an m word block and has a greater gain for Feistel codes where the number of rounds is greater. We use the name GDES for the codes we discuss. The principle can be used on any Feistel code. TEA, a Tiny Encryption Algorithm We design a short program which will run on most machines and encypher safely. It uses a large number of iterations rather than a complicated program. It is hoped that it can easily be translated into most languages in a compatible way. The first program is given below. It uses little set up time and does a weak non linear iteration enough rounds to make it secure. There are no preset tables or long set up times. It assumes 32 bit words. Simple, proven approaches to text retrieval Robertson, S.E. Spärck Jones, K. University of Cambridge, Computer Laboratory 1994-12 en Text UCAM-CL-TR-356 ISSN 1476-2986 This technical note describes straightforward techniques for document indexing and retrieval that have been solidly established through extensive testing and are easy to apply. They are useful for many different types of text material, are viable for very large files, and have the advantage that they do not require special skills or training for searching, but are easy for end users. Seven more myths of formal methods Bowen, Jonathan P. Hinchey, Michael G. University of Cambridge, Computer Laboratory 1994-12 en Text UCAM-CL-TR-357 ISSN 1476-2986 Multithreaded processor design Moore, Simon William University of Cambridge, Computer Laboratory 1995-02 en Text UCAM-CL-TR-358 ISSN 1476-2986 A case study of co-induction in Isabelle Frost, Jacob University of Cambridge, Computer Laboratory 1995-02 en Text UCAM-CL-TR-359 ISSN 1476-2986 The consistency of the dynamic and static semantics for a small functional programming language was informally proved by R. Milner and M. Tofte. The notions of co-inductive definitions and the associated principle of co-induction played a pivotal role in the proof. With emphasis on co-induction, the work presented here deals with the formalisation of this result in the generic theorem prover Isabelle. On the calculation of explicit polymetres Clocksin, W.F. University of Cambridge, Computer Laboratory 1995-03 en Text UCAM-CL-TR-360 ISSN 1476-2986 Computer scientists take an interest in objects or events which can be counted, grouped, timed and synchronised. The computational problems involved with the interpretation and notation of musical rhythm are therefore of particular interest, as the most complex time-stamped structures yet devised by humankind are to be found in music notation. These problems are brought into focus when considering explicit polymetric notation, which is the concurrent use of different time signatures in music notation. While not in common use the notation can be used to specify complicated cross-rhythms, simple versus compound metres, and unequal note values without the need for tuplet notation. From a computational point of view, explicit polymetric notation is a means of specifying synchronisation relationships amongst multiple time-stamped streams. Human readers of explicit polymetic notation use the time signatures together with the layout of barlines and musical events as clues to determine the performance. However, if the aim is to lay out the notation (such as might be required by an automatic music notation processor), the location of barlines and musical events will be unknown, and it is necessary to calculate them given only the information conveyed by the time signatures. Similar problems arise when trying to perform the notation (i.e. animate the specification) in real-time. Some problems in the interpretation of explicit polymetric notation are identified and a solution is proposed. Two different interpretations are distinguished, and methods for their automatic calculation are given. The solution given may be applied to problems which involve the synchronisation or phase adjustment of multiple independent threads of time-stamped objects. Explicit network scheduling Black, Richard John University of Cambridge, Computer Laboratory 1995-04 en Text UCAM-CL-TR-361 ISSN 1476-2986 This dissertation considers various problems associated with the scheduling and network I/O organisation found in conventional operating systems for effective support for multimedia applications which require Quality of Service. A solution for these problems is proposed in a micro-kernel structure. The pivotal features of the proposed design are that the processing of device interrupts is performed by user-space processes which are scheduled by the system like any other, that events are used for both inter- and intra-process synchronisation, and the use of a specially developed high performance I/O buffer management system. An evaluation of an experimental implementation is included. In addition to solving the scheduling and networking problems addressed, the prototype is shown to out-perform the Wanda system (a locally developed micro-kernel) on the same platform. This dissertation concludes that it is possible to construct an operating system where the kernel provides only the fundamental job of fine grain sharing of the CPU between processes, and hence synchronisation between those processes. This enables processes to perform task specific optimisations; as a result system performance is enhanced, both with respect to throughput and the meeting of soft real-time guarantees. W-learning: competition among selfish Q-learners Humphrys, Mark University of Cambridge, Computer Laboratory 1995-04 en Text UCAM-CL-TR-362 ISSN 1476-2986 W-learning is a self-organising action-selection scheme for systems with multiple parallel goals, such as autonomous mobile robots. It uses ideas drawn from the subsumption architecture for mobile robots (Brooks), implementing them with the Q-learning algorithm from reinforcement learning (Watkins). Brooks explores the idea of multiple sensing-and-acting agents within a single robot, more than one of which is capable of controlling the robot on its own if allowed. I introduce a model where the agents are not only autonomous, but are in fact engaged in direct competition with each other for control of the robot. Interesting robots are ones where no agent achieves total victory, but rather the state-space is fragmented among different agents. Having the agents operate by Q-learning proves to be a way to implement this, leading to a local, incremental algorithm (W-learning) to resolve competition. I present a sketch proof that this algorithm converges when the world is a discrete, finite Markov decision process. For each state, competition is resolved with the most likely winner of the state being the agent that is most likely to suffer the most if it does not win. In this way, W-learning can be viewed as ‘fair’ resolution of competition. In the empirical section, I show how W-learning may be used to define spaces of agent-collections whose action selection is learnt rather than hand-designed. This is the kind of solution-space that may be searched with a genetic algorithm. Names and higher-order functions Stark, Ian University of Cambridge, Computer Laboratory 1995-04 en Text UCAM-CL-TR-363 ISSN 1476-2986 Many functional programming languages rely on the elimination of ‘impure’ features: assignment to variables, exceptions and even input/output. But some of these are genuinely useful, and it is of real interest to establish how they can be reintroducted in a controlled way. This dissertation looks in detail at one example of this: the addition to a functional language of dynamically generated “names”. Names are created fresh, they can be compared with each other and passed around, but that is all. As a very basic example of “state”, they capture the graduation between private and public, local and global, by their interaction with higher-order functions. The vehicle for this study is the “nu-calculus”, an extension of the simply-typed lambda-calculus. The nu-calculus is equivalent to a certain fragment of Standard ML, omitting side-effects, exceptions, datatypes and recursion. Even without all these features, the interaction of name creation with higher-order functions can be complex and subtle. Various operational and denotational methods for reasoning about the nu-calculus are developed. These include a computational metalanguage in the style of Moggi, which distinguishes in the type system between values and computations. This leads to categorical models that use a strong monad, and examples are devised based on functor categories. The idea of “logical relations” is used to derive powerful reasoning methods that capture some of the distinction between private and public names. These techniques are shown to be complete for establishing contextual equivalence between first-order expressions; they are also used to construct a correspondingly abstract categorical model. All the work with the nu-calculus extends cleanly to Reduced ML, a larger language that introduces integer references: mutable storage cells that are dynamically allocated. It turns out that the step up is quite simple, and both the computational metalanguage and the sample categorical models can be reused. The Church-Rosser theorem in Isabelle: a proof porting experiment Rasmussen, Ole University of Cambridge, Computer Laboratory 1995-04 en Text UCAM-CL-TR-364 ISSN 1476-2986 This paper describes a proof of the Church-Rosser theorem for the pure lambda-calculus formalised in the Isabelle theorem prover. The initial version of the proof is ported from a similar proof done in the Coq proof assistant by Girard Huet, but a number of optimisations have been performed. The development involves the introduction of several inductive and recursive definitions and thus gives a good presentation of the inductive package of Isabelle. Computational types from a logical perspective I Benton, P.N. Bierman, G.M. de Paiva, V.C.V. University of Cambridge, Computer Laboratory 1995-05 en Text UCAM-CL-TR-365 ISSN 1476-2986 Retrieving spoken documents: VMR Project experiments Spärck Jones, K. Jones, G.J.F. Foote, J.T. Young, S.J. University of Cambridge, Computer Laboratory 1995-05 en Text UCAM-CL-TR-366 ISSN 1476-2986 Categorical logic Pitts, Andrew M. University of Cambridge, Computer Laboratory 1995-05 en Text UCAM-CL-TR-367 ISSN 1476-2986 This document provides an introduction to the interaction between category theory and mathematical logic which is slanted towards computer scientists. It will be a chapter in the forthcoming Volume VI of: S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds), “Handbook of Logic in Computer Science”, Oxford University Press. CogPiT – configuration of protocols in TIP Stiller, Burkhard University of Cambridge, Computer Laboratory 1995-06 en Text UCAM-CL-TR-368 ISSN 1476-2986 The variety of upcoming applications in terms of their performance and Quality-of-Service (QoS) requirements is increasing. Besides almost well-known applications, such as teleconferencing, audio- and video-transmissions, even more contemporary ones, such as medical imaging, Video-on-Demand, and interactive tutoring systems, are introduced and applied to existing networks. On the contrary, traditionally data-oriented applications, such as file transfer and remote login, are considerably different in terms of their QoS requirements. Therefore, the consequences of this evolution effect the architectures of end-systems, e.g., workstations that have to be capable of maintaining all different kinds of multi-media data, and intermediate-systems as well. Therefore, a configuration approach of communication protocols has been developed to support the variety of applications. This approach offers the possibility to configure communication protocols automatically depending on the application requirements expressed in various QoS parameters. The result, an application-tailored communication protocol, matches the requested application requirements as far as possible. Additionally, network and system resources (NSR) are taken into account for a well-suited configuration. The Configuration of Protocols in TIP is called CogPiT and is part of the Transport and Internetworking Package (TIP). As an example, in the TIP environment the transport protocol TEMPO is used for configuration purposes. A comparison of HOL-ST and Isabelle/ZF Agerholm, Sten University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-369 ISSN 1476-2986 The use of higher order logic (simple type theory) is often limited by its restrictive type system. Set theory allows many constructions on sets that are not possible on types in higher order logic. This paper presents a comparison of two theorem provers supporting set theory, namely HOL-ST and Isabelle/ZF, based on a formalization of the inverse limit construction of domain theory; this construction cannot be formalized in higher order logic directly. We argue that whilst the combination of higher order logic and set theory in HOL-ST has advantages over the first order set theory in Isabelle/ZF, the proof infrastructure of Isabelle/ZF has better support for set theory proofs than HOL-ST. Proofs in Isabelle/ZF are both considerably shorter and easier to write. A package for non-primitive recursive function definitions in HOL Agerholm, Sten University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-370 ISSN 1476-2986 LIMINF convergence in Ω-categories Wagner, Kim Ritter University of Cambridge, Computer Laboratory 1995-06 en Text UCAM-CL-TR-371 ISSN 1476-2986 A brief history of mobile telephony Hild, Stefan G. University of Cambridge, Computer Laboratory 1995-01 en Text UCAM-CL-TR-372 ISSN 1476-2986 Natural-language processing and requirements specifications Macías, Benjamín Pulman, Stephen G. University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-373 ISSN 1476-2986 A framework for QoS updates in a networking environment Stiller, Burkhard University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-374 ISSN 1476-2986 The support of sufficient Quality-of-Service (QoS) for applications residing in a distributed environment and running on top of high performance networks is a demanding issue. Currently, the areas to provide this support adequately include communication protocols, operating systems support, and offered network services. A configurable approach of communication protocols offers the needed protocol flexibility to react accordingly on various different requirements. Communication protocols and operating systems have to be parametrized using internal configuration parameters, such as window sizes, retry counters, or scheduling mechanisms, that rely closely on requested application-oriented or network-dependent QoS, such as bandwidth or delay. Moreover, these internal parameters have to be recalculated from time to time due to network changes (such as congestion or line break-down) or due to application-specific alterations (such as enhanced bandwidth requirements or increased reliability) to adjust a temporary or semi-permanent “out-of-tune” service behavior. Therefore, a rule-based evaluation and QoS updating framework for configuration parameters in a networking environment has been developed. The resulting “rulework” can be used within highly dynamic environments in a communication subsystem that offers the possibility to specify for every QoS parameter both a bounding interval of values and an average value. As an example, the framework has been integrated in the Function-based Communication Subsystem (F-CSS). Especially, an enhanced application service interface is offered, allowing for the specification of various QoS-parameters that are used to configure a sufficient application-tailored communication protocol. Restructuring virtual memory to support distributed computing environments Huang, Feng University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-375 ISSN 1476-2986 The structure of a multi-service operating system Roscoe, Timothy University of Cambridge, Computer Laboratory 1995-08 en Text UCAM-CL-TR-376 ISSN 1476-2986 Increases in processor speed and network bandwidth have led to workstations being used to process multimedia data in real time. These applications have requirements not met by existing operating systems, primarily in the area of resource control: there is a need to reserve resources, in particular the processor, at a fine granularity. Furthermore, guarantees need to be dynamically renegotiated to allow users to reassign resources when the machine is heavily loaded. There have been few attempts to provide the necessary facilities in traditional operating systems, and the internal structure of such systems makes the implementation of useful resource control difficult. This dissertation presents a way of structuring an operating system to reduce crosstalk between applications sharing the machine, and enable useful resource guarantees to be made: instead of system services being located in the kernel or server processes, they are placed as much as possible in client protection domains and scheduled as part of the client, with communication between domains only occurring when necessary to enforce protection and concurrency control. This amounts to multiplexing the service at as low a level of abstraction as possible. A mechanism for sharing processor time between resources is also described. The prototype Nemesis operating system is used to demonstrate the ideas in use in a practical system, and to illustrate solutions to several implementation problems that arise. Firstly, structuring tools in the form of typed interfaces within a single address space are used to reduce the complexity of the system from the programmer’s viewpoint and enable rich sharing of text and data between applications. Secondly, a scheduler is presented which delivers useful Quality of Service guarantees to applications in a highly efficient manner. Integrated with the scheduler is an inter-domain communication system which has minimal impact on resource guarantees, and a method of decoupling hardware interrupts from the execution of device drivers. Finally, a framework for high-level inter-domain and inter-machine communication is described, which goes beyond object-based RPC systems to permit both Quality of Service negotiation when a communication binding is established, and services to be implemented straddling protection domain boundaries as well as locally and in remote processes. Mechanising set theory: cardinal arithmetic and the axiom of choice Paulson, Larry Grabczewski, Krzysztof University of Cambridge, Computer Laboratory 1995-07 en Text UCAM-CL-TR-377 ISSN 1476-2986 Fairly deep results of Zermelo-Fraenkel (ZF) set theory have been mechanised using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplication is K*K=K, where K is any infinite cardinal. Proving this result required developing theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc.; this covers most of Kunen, Set Theory, Chapter I. Furthermore, we have proved the equivalence of 7 formulations of the Well-ordering Theorem and 20 formulations of AC; this covers the first two chapters of Rubin and Rubin, Equivalents of the Axiom of Choice. The definitions used in the proofs are largely faithful in style to the original mathematics. Performance evaluation of HARP: a hierarchical asynchronous replication protocol for large scale system Adly, Noha University of Cambridge, Computer Laboratory 1995-08 en Text UCAM-CL-TR-378 ISSN 1476-2986 Proceedings of the First Isabelle Users Workshop Paulson, Lawrence University of Cambridge, Computer Laboratory 1995-09 en Text UCAM-CL-TR-379 ISSN 1476-2986 Quality-of-Service issues in networking environments Stiller, Burkhard University of Cambridge, Computer Laboratory 1995-09 en Text UCAM-CL-TR-380 ISSN 1476-2986 Quality-of-Service (QoS) issues in networking environments cover various separate areas and topics. They include at least the specification of applications requirements, the definition of network services, QoS models, resource reservation methods, negotiation and transformation methods for QoS, and operating system support for guaranteed services. An embracing approach for handling, dealing with, and supporting QoS in different scenarios and technical set-ups is required to manage sufficiently forthcoming communication and networking tasks. Modern telecommunication systems require an integrated architecture for applications, communication subsystems, and network perspectives to overcome drawbacks of traditional communication architectures, such as redundant protocol functionality, weakly designed interfaces between the end-system and a network adapter, or impossibility of specifying and guaranteeing QoS parameter. This work contains the discussion of a number of interconnected QoS issues, e.g., QoS mapping, QoS negotiation, QoS-based configuration of communication protocols, or QoS aspects in Asynchronous Transfer Mode (ATM) signaling protocols, which have been dealt with during a one-year research fellowship. This report is not intended to be a complete description of every technical detail, but tries to provide a brief overall picture of the emerging and explosively developing QoS issues in telecommunication systems. Additionally, investigations of some of these issues are undertaken in a more closer detail. It is mainly focussed on QoS mapping, negotiation, and updating in the communication protocol area. Rendering for free form deformations Nimscheck, Uwe Michael University of Cambridge, Computer Laboratory 1995-10 en Text UCAM-CL-TR-381 ISSN 1476-2986 Synthetic image generation for a multiple-view autostereo display Castle, Oliver M. University of Cambridge, Computer Laboratory 1995-10 en Text UCAM-CL-TR-382 ISSN 1476-2986 Management of replicated data in large scale systems Adly, Noha University of Cambridge, Computer Laboratory 1995-11 en Text UCAM-CL-TR-383 ISSN 1476-2986 Securing ATM networks Chuang, Shaw-Cheng University of Cambridge, Computer Laboratory 1995-01 en Text UCAM-CL-TR-384 ISSN 1476-2986 This is an interim report on the investigations into securing Asynchronous Transfer Mode (ATM) networks. We look at the challenge in providing such a secure ATM network and identify the important issues in achieving such goal. In this paper, we discuss the issues and problems involved and outline some techniques to solving these problems. The network environment is first examined and we also consider the correct placement of security mechanism in such an environment. Following the analysis of the security requirement, we introduce and describe a key agile cryptographic device for ATM. The protection of the ATM data plane is extremely important to provide data confidentiality and data integrity. Techniques in providing synchronisation, dynamic key change, dynamic initialisation vector change and Message Authentication Code on ATM data, are also being considered. Next, we discuss the corresponding control functions. A few key exchange protocols are given as possible candidates for the establishment of the session key. The impact of such key exchange protocols on the design of an ATM signalling protocol has also been examined and security extension to an existing signalling protocol being discussed. We also talk about securing other control plane functions such as NNI routing, Inter-Domain Policy Routing, authorisation and auditing, firewall and intrusion detection, Byzantine robustness. Management plane functions are also being looked at, with discussions on bootstrapping, authenticated neighbour discovery, ILMI Security, PVC security, VPI security and ATM Forum management model. Performance evaluation of the Delphi machine Saraswat, Sanjay University of Cambridge, Computer Laboratory 1995-12 en Text UCAM-CL-TR-385 ISSN 1476-2986 Bisimilarity for a first-order calculus of objects with subtyping Gordon, Andrew D. Rees, Gareth D. University of Cambridge, Computer Laboratory 1996-01 en Text UCAM-CL-TR-386 ISSN 1476-2986 Monitoring composite events in distributed systems Schwiderski, Scarlet Herbert, Andrew Moody, Ken University of Cambridge, Computer Laboratory 1996-02 en Text UCAM-CL-TR-387 ISSN 1476-2986 A unified approach to strictness analysis and optimising transformations Benton, P.N. University of Cambridge, Computer Laboratory 1996-02 en Text UCAM-CL-TR-388 ISSN 1476-2986 A proof checked for HOL Wong, Wai University of Cambridge, Computer Laboratory 1996-03 en Text UCAM-CL-TR-389 ISSN 1476-2986 Syn: a single language for specifiying abstract syntax tress, lexical analysis, parsing and pretty-printing Boulton, Richard J. University of Cambridge, Computer Laboratory 1996-03 en Text UCAM-CL-TR-390 ISSN 1476-2986 A language called Syn is described in which all aspects of context-free syntax can be specified without redundancy. The language is essentially an extended BNF grammar. Unusual features include high-level constructs for specifying lexical aspects of a language and specification of precedence by textual order. A system has been implemented for generating lexers, parsers, pretty-printers and abstract syntax tree representations from a Syn specification. Programming languages and dimensions Kennedy, Andrew John University of Cambridge, Computer Laboratory 1996-04 en Text UCAM-CL-TR-391 ISSN 1476-2986 Decoding choice encodings Nestmann, Uwe Pierce, Benjamin C. University of Cambridge, Computer Laboratory 1996-04 en Text UCAM-CL-TR-392 ISSN 1476-2986 Performance management in ATM networks Crosby, Simon Andrew University of Cambridge, Computer Laboratory 1996-04 en Text UCAM-CL-TR-393 ISSN 1476-2986 The Asynchronous Transfer Mode (ATM) has been identified as the technology of choice amongst high speed communication networks for its potential to integrate services with disparate resource needs and timing constraints. Before it can successfully deliver integrated services, however, significant problems remain to be solved. They centre around two major issues. First, there is a need for a simple, powerful network service interface capable of meeting the communications needs of new applications. Second, within the network there is a need to dynamically control a mix of diverse traffic types to ensure that they meet their performance criteria. Addressing the first concern, this dissertation argues that a simple network control interface offers significant advantages over the traditional, heavyweight approach of the telecommunications industry. A network control architecture based on a distributed systems approach is presented which locates both the network control functions and its services outside the network. The network service interface uses the Remote Procedure Call (RPC) paradigm and enables more complicated service offerings to be built from the basic primitives. A formal specification and verification of the user-network signalling protocol is presented. Implementations of the architecture, both on Unix and the Wanda micro-kernel, used on the Fairisle ATM switch, are described. The implementations demonstrate the feasibility of the architecture, and feature a high degree of experimental flexibility. This is exploited in the balance of the dissertation, which presents the results of a practical study of network performance under a range of dynamic control mechanisms. Addressing the second concern, results are presented from a study of the cell delay variation suffered by ATM connections when multiplexed with real ATM traffic in an uncontrolled network, and from an investigation of the expansion of bursts of ATM traffic as a result of multiplexing. The results are compared with those of analytical models. Finally, results from a study of the performance delivered to delay sensitive traffic by priority and rate based cell scheduling algorithms, and the loss experienced by different types of traffic under several buffer allocation strategies are presented. A simple formalization and proof for the mutilated chess board Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1996-04 en Text UCAM-CL-TR-394 ISSN 1476-2986 The impossibility of tiling the mutilated chess board has been formalized and verified using Isabelle. The formalization is concise because it is expressed using inductive definitions. The proofs are straightforward except for some lemmas concerning finite cardinalities. This exercise is an object lesson in choosing a good formalization. is applicable in a variety of domains. Cut-elimination for full intuitionistic linear logic Bräuner, Torben de Paiva, Valeria University of Cambridge, Computer Laboratory 1996-05 en Text UCAM-CL-TR-395 ISSN 1476-2986 Generic automatic proof tools Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1996-05 en Text UCAM-CL-TR-396 ISSN 1476-2986 This paper explores a synthesis between two distinct traditions in automated reasoning: resolution and interaction. In particular it discusses Isabelle, an interactive theorem prover based upon a form of resolution. It aims to demonstrate the value of proof tools that, compared with traditional resolution systems, seem absurdly limited. Isabelle’s classical reasoner searches for proofs using a tableau approach. The reasoner is generic: it accepts rules proved in applied theories, involving defined connectives. New constants are not reduced to first-order logic; the reasoner Optimal routing in 2-jump circulant networks Robič, Borut University of Cambridge, Computer Laboratory 1996-06 en Text UCAM-CL-TR-397 ISSN 1476-2986 An algorithm for routing a message along the shortest path between a pair of processors in 2-jump circulant (undirected double fixed step) network is given. The algorithm requires O(d) time for preprocessing, and l = O(d) routing steps, where l is the distance between the processors and d is the diameter of the network. Design and implementation of an autostereoscopic camera system Dodgson, N.A. Moore, J.R. University of Cambridge, Computer Laboratory 1996-06 en Text UCAM-CL-TR-398 ISSN 1476-2986 An autostereoscopic display provides the viewer with a three-dimensional image without the need for special glasses, and allows the user to look around objects in the image by moving the head left-right. The time-multiplexed autostereo display developed at the University of Cambridge has been in operation since late 1991. An autostereoscopic camera system has been designed and implemented. It is capable of taking video input from up to sixteen cameras, and multiplexing these into a video output stream with a pixel rate an order of magnitude faster than the individual input streams. Testing of the system with eight cameras and a Cambridge Autostereo Display has produced excellent live autostereoscopic video. This report describes the design of this camera system which has been successfully implemented and demonstrated. Problems which arose during this process are discussed, and a comparison with similar systems made. OASIS : An open architecture for secure interworking services Hayton, Richard University of Cambridge, Computer Laboratory 1996-06 en Text UCAM-CL-TR-399 ISSN 1476-2986 An emerging requirement is for applications and distributed services to cooperate or inter-operate. Mechanisms have been devised to hide the heterogeneity of the host operating systems and abstract the issues of distribution and object location. However, in order for systems to inter-operate securely there must also be mechanisms to hide differences in security policy, or at least negotiate between them. This would suggest that a uniform model of access control is required. Such a model must be extremely flexible with respect to the specification of policy, as different applications have radically different needs. In a widely distributed environment this situation is exacerbated by the differing requirements of different organisations, and in an open environment there is a need to interwork with organisations using alternative security mechanisms. Other proposals for the interworking of security mechanisms have concentrated on the enforcement of access policy, and neglected the concerns of freedom of expression of this policy. For example it is common to associate each request with a user identity, and to use this as the only parameter when performing access control. This work describes an architectural approach to security. By reconsidering the role of the client and the server, we may reformulate access control issues in terms of client naming. We think of a client as obtaining a name issued by a service; either based on credentials already held by the client, or by delegation from another client. A grammar has been devised that allows the conditions under which a client may assume a name to be specified, and the conditions under which use of the name will be revoked. This allows complex security policies to be specified that define how clients of a service may interact with each other (through election, delegation and revocation), how clients interact with a service (by invoking operations or receiving events) and how clients and services may inter-operate. (For example, a client of a Login service may become a client of a file service.) This approach allows great flexibility when integrating a number of services, and reduces the mismatch of policies common in heterogeneous systems. A flexible security definition is meaningless if not backed by a robust and efficient implementation. In this thesis we present a systems architecture that can be implemented efficiently, but that allows individual services to ‘fine tune’ the trade-offs between security, efficiency and freedom of policy expression. The architecture is inherently distributed and scalable, and includes mechanisms for rapid and selective revocation of privileges which may cascade between services and organisations. Monitoring the behaviour of distributed systems Schwiderski, Scarlet University of Cambridge, Computer Laboratory 1996-07 en Text UCAM-CL-TR-400 ISSN 1476-2986 A classical linear λ-calculus Bierman, Gavin University of Cambridge, Computer Laboratory 1996-07 en Text UCAM-CL-TR-401 ISSN 1476-2986 Video mail retrieval using voice: report on collection of naturalistic requests and relevance assessments Jones, G.J.F. Foote, J.T. Spärck Jones, K. Young, S.J. University of Cambridge, Computer Laboratory 1996-09 en Text UCAM-CL-TR-402 ISSN 1476-2986 Devices in a multi-service operating system Barham, Paul Ronald University of Cambridge, Computer Laboratory 1996-10 en Text UCAM-CL-TR-403 ISSN 1476-2986 Increases in processor speed and network and device bandwidth have led to general purpose workstations being called upon to process continuous media data in real time. Conventional operating systems are unable to cope with the high loads and strict timing constraints introduced when such applications form part of a multi-tasking workload. There is a need for the operating system to provide fine-grained reservation of processor, memory and I/O resources and the ability to redistribute these resources dynamically. A small group of operating systems researchers have recently proposed a “vertically-structured” architecture where the operating system kernel provides minimal functionality and the majority of operating system code executes within the application itself. This structure greatly simplifies the task of accounting for processor usage by applications. The prototype Nemesis operating system embodies these principles and is used as the platform for this work. This dissertation extends the provision of Quality of Service guarantees to the I/O system by presenting an architecture for device drivers which minimises crosstalk between applications. This is achieved by clearly separating the data-path operations, which require careful accounting and scheduling, and the infrequent control-path operations, which require protection and concurrency control. The approach taken is to abstract and multiplex the I/O data-path at the lowest level possible so as to simplify accounting, policing and scheduling of I/O resources and enable application-specific use of I/O devices. The architecture is applied to several representative classes of device including network interfaces, network connected peripherals, disk drives and framestores. Of these, disks and framestores are of particular interest since they must be shared at a very fine granularity but have traditionally been presented to the application via a window system or file-system with a high-level and coarse-grained interface. A device driver for the framestore is presented which abstracts the device at a low level and is therefore able to provide each client with guaranteed bandwidth to the framebuffer. The design and implementation of a novel client-rendering window system is then presented which uses this driver to enable rendering code to be safely migrated into a shared library within the client. A low-level abstraction of a standard disk drive is also described which efficiently supports a wide variety of file systems and other applications requiring persistent storage, whilst providing guaranteed rates of I/O to individual clients. An extent-based file system is presented which can provide guaranteed rate file access and enables clients to optimise for application-specific access patterns. Adaptive parallelism for computing on heterogeneous clusters Shum, Kam Hong University of Cambridge, Computer Laboratory 1996-11 en Text UCAM-CL-TR-404 ISSN 1476-2986 A tool to support formal reasoning about computer languages Boulton, Richard J. University of Cambridge, Computer Laboratory 1996-11 en Text UCAM-CL-TR-405 ISSN 1476-2986 A tool to support formal reasoning about computer languages and specific language texts is described. The intention is to provide a tool that can build a formal reasoning system in a mechanical theorem prover from two specifications, one for the syntax of the language and one for the semantics. A parser, pretty-printer and internal representations are generated from the former. Logical representations of syntax and semantics, and associated theorem proving tools, are generated from the combination of the two specifications. The main aim is to eliminate tedious work from the task of prototyping a reasoning tool for a computer language, but the abstract specifications of the language also assist the automation of proof. Tool support for logics of programs Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1996-11 en Text UCAM-CL-TR-406 ISSN 1476-2986 Proof tools must be well designed if they are to be more effective than pen and paper. Isabelle supports a range of formalisms, two of which are described (higher-order logic and set theory). Isabelle’s representation of logic is influenced by logic programming: its “logical variables” can be used to implement step-wise refinement. Its automatic proof procedures are based on search primitives that are directly available to users. While emphasizing basic concepts, the article also discusses applications such as an approach to the analysis of security protocols. The L4 microkernel on Alpha : Design and implementation Schoenberg, Sebastian University of Cambridge, Computer Laboratory 1996-09 en Text UCAM-CL-TR-407 ISSN 1476-2986 The purpose of a microkernel is to cover the lowest level of the hardware and to provide a more general platform to operating systems and applications than the hardware itself. This has made microkernel development increasingly interesting. Different types of microkernels have been developed, ranging from kernels which merely deal with the hardware infterface (Windows NT HAL), kernels especially for embedded systems (RTEMS), to kernels for multimedia streams and real time support (Nemesis) and general purpose kernels (L4, Mach). The common opinion that microkernels lead to deterioration in system performance has been disproved by recent research. L4 is an example of a fast and small, multi address space, message-based microkernel, developed originally for Intel systems only. Based on the L4 interface, which should be as similar as possible on different platforms, the L4 Alpha version has been developed. This work describes design decisions, implementation and interfaces of the L4 version for 64-bit Alpha processors. Theorem proving with the real numbers Harrison, John Robert University of Cambridge, Computer Laboratory 1996-11 en Text UCAM-CL-TR-408 ISSN 1476-2986 This thesis discusses the use of the real numbers in theorem proving. Typically, theorem provers only support a few ‘discrete’ datatypes such as the natural numbers. However the availability of the real numbers opens up many interesting and important application areas, such as the verification of floating point hardware and hybrid systems. It also allows the formalization of many more branches of classical mathematics, which is particularly relevant for attempts to inject more rigour into computer algebra systems. Our work is conducted in a version of the HOL theorem prover. We describe the rigorous definitional construction of the real numbers, using a new version of Cantor’s method, and the formalization of a significant portion of real analysis. We also describe an advanced derived decision procedure for the ‘Tarski subset’ of real algebra as well as some more modest but practically useful tools for automating explicit calculations and routine linear arithmetic reasoning. Finally, we consider in more detail two interesting application areas. We discuss the desirability of combining the rigour of theorem provers with the power and convenience of computer algebra systems, and explain a method we have used in practice to achieve this. We then move on to the verification of floating point hardware. After a careful discussion of possible correctness specifications, we report on two case studies, one involving a transcendental function. We aim to show that a theory of real numbers is useful in practice and interesting in theory, and that the ‘LCF style’ of theorem proving is well suited to the kind of work we describe. We hope also to convince the reader that the kind of mathematics needed for applications is well within the abilities of current theorem proving technology. Proving properties of security protocols by induction Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1996-12 en Text UCAM-CL-TR-409 ISSN 1476-2986 Security protocols are formally specified in terms of traces, which may involve many interleaved protocol runs. Traces are defined inductively. Protocol descriptions model accidental key losses as well as attacks. The model spy can send spoof messages made up of components decrypted from previous traffic. Correctness properties are verified using the proof tool Isabelle/HOL. Several symmetric-key protocols have been studied, including Needham-Schroeder, Yahalom and Otway-Rees. A new attack has been discovered in a variant of Otway-Rees (already broken by Mao and Boyd). Assertions concerning secrecy and authenticity have been proved. The approach rests on a common theory of messages, with three operators. The operator “parts” denotes the components of a set of messages. The operator “analz” denotes those parts that can be decrypted with known keys. The operator “synth” denotes those messages that can be expressed in terms of given components. The three operators enjoy many algebraic laws that are invaluable in proofs. Proof style Harrison, John University of Cambridge, Computer Laboratory 1997-01 en Text UCAM-CL-TR-410 ISSN 1476-2986 We are concerned with how to communicate a mathematical proof to a computer theorem prover. This can be done in many ways, while allowing the machine to generate a completely formal proof object. The most obvious choice is the amount of guidance required from the user, or from the machine perspective, the degree of automation provided. But another important consideration, which we consider particularly significant, is the bias towards a ‘procedural’ or ‘declarative’ proof style. We will explore this choice in depth, and discuss the strengths and weaknesses of declarative and procedural styles for proofs in pure mathematics and for verification applications. We conclude with a brief summary of our own experiments in trying to combine both approaches. Formalising process calculi in Higher Order Logic Nesi, Monica University of Cambridge, Computer Laboratory 1997-01 en Text UCAM-CL-TR-411 ISSN 1476-2986 Observations on a linear PCF (preliminary report) Bierman, G.M. University of Cambridge, Computer Laboratory 1997-01 en Text UCAM-CL-TR-412 ISSN 1476-2986 Mechanized proofs of security protocols: Needham-Schroeder with public keys Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1997-01 en Text UCAM-CL-TR-413 ISSN 1476-2986 The inductive approach to verifying security protocols, previously applied to shared-key encryption, is here applied to the public key version of the Needham-Schroeder protocol. As before, mechanized proofs are performed using Isabelle/HOL. Both the original, flawed version and Lowe’s improved version are studied; the properties proved highlight the distinctions between the two versions. The results are compared with previous analyses of the same protocol. The analysis reported below required only 30 hours of the author’s time. The proof scripts execute in under three minutes. A calculus for cryptographic protocols : The SPI calculus Abadi, Martín Gordon, Andrew D. University of Cambridge, Computer Laboratory 1997-01 en Text UCAM-CL-TR-414 ISSN 1476-2986 We introduce the spi calculus, an extension of the pi calculus designed for the description and analysis of cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence. Application support for mobile computing Pope, Steven Leslie University of Cambridge, Computer Laboratory 1997-02 en Text UCAM-CL-TR-415 ISSN 1476-2986 DECLARE: a prototype declarative proof system for higher order logic Syme, Donald University of Cambridge, Computer Laboratory 1997-02 en Text UCAM-CL-TR-416 ISSN 1476-2986 Selective mesh refinement for interactive terrain rendering Brown, Peter J.C. University of Cambridge, Computer Laboratory 1997-02 en Text UCAM-CL-TR-417 ISSN 1476-2986 Terrain surfaces are often approximated by geometric meshes to permit efficient rendering. This paper describes how the complexity of an approximating irregular mesh can be varied across its domain in order to minimise the number of displayed facets while ensuring that the rendered surface meets pre-determined resolution requirements. We first present a generalised scheme to represent a mesh over a continuous range of resolutions using the output from conventional single-resolution approximation methods. We then describe an algorithm which extracts a surface from this representation such that the resolution of the surface is enhanced only in specific areas of interest. We prove that the extracted surface is complete, minimal, satisfies the given resolution constraints and meets the Delaunay triangulation criterion if possible. In addition, we present a method of performing smooth visual transitions between selectively-refined meshes to permit efficient animation of a terrain scene. A HTML version of that report is at http://www.cl.cam.ac.uk/research/rainbow/publications/pjcb/tr417/ Mechanized proofs for a recursive authentication protocol Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1997-03 en Text UCAM-CL-TR-418 ISSN 1476-2986 A novel protocol has been formally analyzed using the prover Isabelle/HOL, following the inductive approach described in earlier work. There is no limit on the length of a run, the nesting of messages or the number of agents involved. A single run of the protocol delivers session keys for all the agents, allowing neighbours to perform mutual authentication. The basic security theorem states that session keys are correctly delivered to adjacent pairs of honest agents, regardless of whether other agents in the chain are compromised. The protocol’s complexity caused some difficulties in the specification and proofs, but its symmetry reduced the number of theorems to prove. Video-augmented environments Stafford-Fraser, James Quentin University of Cambridge, Computer Laboratory 1997-04 en Text UCAM-CL-TR-419 ISSN 1476-2986 In the future, the computer will be thought of more as an assistant than as a tool, and users will increasingly expect machines to make decisions on their behalf. As with a human assistant, a machine’s ability to make informed choices will often depend on the extent of its knowledge of activities in the world around it. Equipping personal computers with a large number of sensors for monitoring their environment is, however, expensive and inconvenient, and a preferable solution would involve a small number of input devices with a broad scope of application. Video cameras are ideally suited to many realworld monitoring applications for this reason. In addition, recent reductions in the manufacturing costs of simple cameras will soon make their widespread deployment in the home and office economically viable. The use of video as an input device also allows the creation of new types of user-interface, more suitable in some circumstances than those afforded by the conventional keyboard and mouse. This thesis examines some examples of these ‘Video-Augmented Environments’ and related work, and then describes two applications in detail. The first, a ‘software cameraman’, uses the analysis of one video stream to control the display of another. The second, ‘BrightBoard’, allows a user to control a computer by making marks on a conventional whiteboard, thus ‘augmenting’ the board with many of the facilities common to electronic documents, including the ability to fax, save, print and email the image of the board. The techniques which were found to be useful in the construction of these applications are common to many systems which monitor real-world video, and so they were combined in a toolkit called ‘Vicar’. This provides an architecture for ‘video plumbing’, which allows standard videoprocessing components to be connected together under the control of a scripting language. It is a single application which can be programmed to create a variety of simple Video-Augmented Environments, such as those described above, without the need for any recompilation, and so should simplify the construction of such applications in the future. Finally, opportunities for further exploration on this theme are discussed. Managing complex models for computer graphics Sewell, Jonathan Mark University of Cambridge, Computer Laboratory 1997-04 en Text UCAM-CL-TR-420 ISSN 1476-2986 Three-dimensional computer graphics is becoming more common as increasing computational power becomes more readily available. Although the images that can be produced are becoming more complex, users’ expectations continue to grow. This dissertation examines the changes in computer graphics software that will be needed to support continuing growth in complexity, and proposes techniques for tackling the problems that emerge. Increasingly complex models will involve longer rendering times, higher memory requirements, longer data transfer periods and larger storage capacities. Furthermore, even greater demands will be placed on the constructors of such models. This dissertation aims to describe how to construct scalable systems which can be used to visualise models of any size without requiring dedicated hardware. This is achieved by controlling the quality of the results, and hence the costs incurred. In addition, the use of quality controls can become a tool to help users handle the large volume of information arising from complex models. The underlying approach is to separate the model from the graphics application which uses it, so that the model exists independently. By doing this, an application is free to access only the data which is required at any given time. For the application to function in this manner, the data must be in an appropriate form. To achieve this, approximation hierarchies are defined as a suitable new model structure. These utilise multiple representations of both objects and groups of objects at all levels in the model. In order to support such a structure, a novel method is proposed for rapidly constructing simplified representations of groups of complex objects. By calculating a few geometrical attributes, it is possible to generate replacement objects that preserve important aspects of the originals. Such objects, once placed into an approximation hierarchy, allow rapid loading and rendering of large portions of a model. Extensions to rendering algorithms are described that take advantage of this structure. The use of multiple representations encompasses not only different quality levels, but also different storage formats and types of objects. It provides a framework within which such aspects are hidden from the user, facilitating the sharing and re-use of objects. A model manager is proposed as a means of encapsulating these mechanisms. This software gives, as far as possible, the illusion of direct access to the whole complex model, while at the same time making the best use of the limited resources available. An abstract dynamic semantics for C Norrish, Michael University of Cambridge, Computer Laboratory 1997-05 en Text UCAM-CL-TR-421 ISSN 1476-2986 This report is a presentation of a formal semantics for the C programming language. The semantics has been defined operationally in a structured semantics style and covers the bulk of the core of the language. The semantics has been developed in a theorem prover (HOL), where some expected consequences of the language definition Using the BONITA primitives: a case study Rowstron, Antony University of Cambridge, Computer Laboratory 1997-05 en Text UCAM-CL-TR-422 ISSN 1476-2986 Symbol grounding : Learning categorical and sensorimotor predictions for coordination in autonomous robots MacDorman, Karl F. University of Cambridge, Computer Laboratory 1997-05 en Text UCAM-CL-TR-423 ISSN 1476-2986 Simplification with renaming: a general proof technique for tableau and sequent-based provers Massacci, Fabio University of Cambridge, Computer Laboratory 1997-05 en Text UCAM-CL-TR-424 ISSN 1476-2986 Should your specification language be typed? Lamport, Leslie Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1997-05 en Text UCAM-CL-TR-425 ISSN 1476-2986 Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased complexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verification, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages. Action selection methods using reinforcement learning Humphrys, Mark University of Cambridge, Computer Laboratory 1997-06 en Text UCAM-CL-TR-426 ISSN 1476-2986 The Action Selection problem is the problem of run-time choice between conflicting and heterogenous goals, a central problem in the simulation of whole creatures (as opposed to the solution of isolated uninterrupted tasks). This thesis argues that Reinforcement Learning has been overlooked in the solution of the Action Selection problem. Considering a decentralised model of mind, with internal tension and competition between selfish behaviors, this thesis introduces an algorithm called “W-learning”, whereby different parts of the mind modify their behavior based on whether or not they are succeeding in getting the body to execute their actions. This thesis sets W-learning in context among the different ways of exploiting Reinforcement Learning numbers for the purposes of Action Selection. It is a ‘Minimize the Worst Unhappiness’ strategy. The different methods are tested and their strengths and weaknesses analysed in an artificial world. Proving Java type soundness Syme, Don University of Cambridge, Computer Laboratory 1997-06 en Text UCAM-CL-TR-427 ISSN 1476-2986 Floating point verification in HOL Light: the exponential function Harrison, John University of Cambridge, Computer Laboratory 1997-06 en Text UCAM-CL-TR-428 ISSN 1476-2986 In that they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing the exponential function in IEEE-754 standard binary floating point arithmetic. We confirm (indeed strengthen) the main result of a previously published error analysis, though we uncover a minor error in the hand proof and are forced to confront several subtle issues that might easily be overlooked informally. Our main theorem connects the floating point exponential to its abstract mathematical counterpart. The specification we prove is that the function has the correct overflow behaviour and, in the absence of overflow, the error in the result is less than 0.54 units in the last place (0.77 if the answer is denormalized) compared against the exact mathematical exponential function. The algorithm is expressed in a simple formalized programming language, intended to be a subset of real programming and hardware description languages. It uses underlying floating point operations (addition, multiplication etc.) that are assumed to conform to the IEEE-754 standard for binary floating point arithmetic. The development described here includes, apart from the proof itself, a formalization of IEEE arithmetic, a mathematical semantics for the programming language in which the algorithm is expressed, and the body of pure mathematics needed. All this is developed logically from first principles using the HOL Light prover, which guarantees strict adherence to simple rules of inference while allowing the user to perform proofs using higher-level derived rules. We first present the main ideas and conclusions, and then collect some technical details about the prover and the underlying mathematical theories in appendices. Compilation and equivalence of imperative objects Gordon, Andrew D. Hankin, Paul D. Lassen, Søren B. University of Cambridge, Computer Laboratory 1997-06 en Text UCAM-CL-TR-429 ISSN 1476-2986 We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus. Our first two results are theorems asserting the equivalence of our substitution-based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott’s CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus. Video mail retrieval using voice : Report on topic spotting Jones, G.J.F. et al. University of Cambridge, Computer Laboratory 1997-07 en Text UCAM-CL-TR-430 ISSN 1476-2986 The MCPL programming manual and user guide Richards, Martin University of Cambridge, Computer Laboratory 1997-07 en Text UCAM-CL-TR-431 ISSN 1476-2986 On two formal analyses of the Yahalom protocol Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1997-07 en Text UCAM-CL-TR-432 ISSN 1476-2986 The Yahalom protocol is one of those analyzed by Burrows et al. in the BAN paper. Based upon their analysis, they have proposed modifications to make the protocol easier to understand and analyze. Both versions of Yahalom have now been proved, using Isabelle/HOL, to satisfy strong security goals. The mathematical reasoning behind these machine proofs is presented informally. The new proofs do not rely on a belief logic; they use an entirely different formal model, the inductive method. They confirm the BAN analysis and the advantages of the proposed modifications. The new proof methods detect more flaws than BAN and analyze protocols in finer detail, while remaining broadly consistent with the BAN principles. In particular, the proofs confirm the explicitness principle of Abadi and Needham. Backtracking algorithms in MCPL using bit patterns and recursion Richards, Martin University of Cambridge, Computer Laboratory 1997-07 en Text UCAM-CL-TR-433 ISSN 1476-2986 Demonstration programs for CTL and μ-calculus symbolic model checking Richards, Martin University of Cambridge, Computer Laboratory 1997-08 en Text UCAM-CL-TR-434 ISSN 1476-2986 Global/local subtyping for a distributed π-calculus Sewell, Peter University of Cambridge, Computer Laboratory 1997-08 en Text UCAM-CL-TR-435 ISSN 1476-2986 A new method for estimating optical flow Clocksin, W.F. University of Cambridge, Computer Laboratory 1997-11 en Text UCAM-CL-TR-436 ISSN 1476-2986 Trusting in computer systems Harbison, William S. University of Cambridge, Computer Laboratory 1997-12 en Text UCAM-CL-TR-437 ISSN 1476-2986 An architecture for scalable and deterministic video servers Shi, Feng University of Cambridge, Computer Laboratory 1997-11 en Text UCAM-CL-TR-438 ISSN 1476-2986 A video server is a storage system that can provide a repository for continuous media (CM) data and sustain CM stream delivery (playback or recording) through networks. The voluminous nature of CM data demands a video server to be scalable in order to serve a large number of concurrent client requests. In addition, deterministic services can be provided by a video server for playback because the characteristics of variable bit rate (VBR) video can be analysed in advance and used in run-time admission control (AC) and data retrieval. Recent research has made gigabit switches a reality, and the cost/performance ratio of microprocessors and standard PCs is dropping steadily. It would be more cost effective and flexible to use off-the-shelf components inside a video server with a scalable switched network as the primary interconnect than to make a special purpose or massively parallel multiprocessor based video server. This work advocates and assumes such a scalable video server structure in which data is striped to multiple peripherals attached directly to a switched network. However, most contemporary distributed file systems do not support data distribution across multiple networked nodes, let alone providing quality of service (QoS) to CM applications at the same time. It is the observation of this dissertation that the software system framework for network striped video servers is as important as the scalable hardware architecture itself. This leads to the development of a new system architecture, which is scalable, flexible and QoS aware, for scalable and deterministic video servers. The resulting srchitecture is called Cadmus from sCAlable and Deterministic MUlitmedia Servers. Cadmus also provides integrated solutions to AC and actual QoS enforcement in storage nodes. This is achieved by considering resources such as CPU buffer, disk, and network, simultaneously but not independently and by including both real-time (RT) and non-real-time (NRT) activities, In addition, the potential to smooth the variability of VBR videos using read-ahead under client buffer constraints is identified. A new smoothing algorithm is presented, analysed, and incorporated into the Cadmus architecture. A prototype implementation of Cadmus has been constructed based on distributed object computing and hardware modules directly connected to an Asynchronous Transfer Mode (ATM) network. Experiments were performed to evaluate the implementation and demonstrate the utility and feasibility of the architecture and its AC criteria. Applying mobile code to distributed systems Halls, David A. University of Cambridge, Computer Laboratory 1997-12 en Text UCAM-CL-TR-439 ISSN 1476-2986 Inductive analysis of the internet protocol TLS Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1997-12 en Text UCAM-CL-TR-440 ISSN 1476-2986 Internet browsers use security protocols to protect confidential messages. An inductive analysis of TLS (a descendant of SSL 3.0) has been performed using the theorem prover Isabelle. Proofs are based on higher-order logic and make no assumptions concerning beliefs or finiteness. All the obvious security goals can be proved; session resumption appears to be secure even if old session keys have been compromised. The analysis suggests modest changes to simplify the protocol. TLS, even at an abstract level, is much more complicated than most protocols that researchers have verified. Session keys are negotiated rather than distributed, and the protocol has many optional parts. Nevertheless, the resources needed to verify TLS are modest. The inductive approach scales up. A generic tableau prover and its integration with Isabelle Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1998-01 en Text UCAM-CL-TR-441 ISSN 1476-2986 A generic tableau prover has been implemented and integrated with Isabelle. It is based on leantap but is much more complicated, with numerous modifications to allow it to reason with any supplied set of tableau rules. It has a higher-order syntax in order to support the binding operators of set theory; unification is first-order (extended for bound variables in obvious ways) instead of higher-order, for simplicity. When a proof is found, it is returned to Isabelle as a list of tactics. Because Isabelle verifies the proof, the prover can cut corners for efficiency’s sake without compromising soundness. For example, it knows almost nothing about types. A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia Fleuriot, Jacques Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1998-01 en Text UCAM-CL-TR-442 ISSN 1476-2986 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) and a powerful geometric theory, we introduce the concept of an infinitesimal geometry in which quantities can be infinitely small or infinitesimal. We reveal and prove new properties of this geometry that only hold because infinitesimal elements are allowed and use them to prove lemmas and theorems from the Principia. The inductive approach to verifying cryptographic protocols Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1998-02 en Text UCAM-CL-TR-443 ISSN 1476-2986 Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state systems. Proofs are generated using Isabelle/HOL. The human effort required to analyze a protocol can be as little as a week or two, yielding a proof script that takes a few minutes to run. Protocols are inductively defined as sets of traces. A trace is a list of communication events, perhaps comprising many interleaved protocol runs. Protocol descriptions incorporate attacks and accidental losses. The model spy knows some private keys and can forge messages using components decrypted from previous traffic. Three protocols are analyzed below: Otway-Rees (which uses shared-key encryption), Needham-Schroeder (which uses public-key encryption), and a recursive protocol (which is of variable length). One can prove that event ev always precedes event ev′ or that property P holds provided X remains secret. Properties can be proved from the viewpoint of the various principals: say, if A receives a final message from B then the session key it conveys is good. From rewrite rules to bisimulation congruences Sewell, Peter University of Cambridge, Computer Laboratory 1998-05 en Text UCAM-CL-TR-444 ISSN 1476-2986 Secure sessions from weak secrets Roe, Michael Christianson, Bruce Wheeler, David University of Cambridge, Computer Laboratory 1998-07 en Text UCAM-CL-TR-445 ISSN 1476-2986 Sometimes two parties who share a weak secret k (such as a password) wish to share a strong secret s (such as a session key) without revealing information about k to a (possibly active) attacker. We assume that both parties can generate strong random numbers and forget secrets, and present three protocols for secure strong secret sharing, based on RSA, Diffie-Hellman and El-Gamal. As well as being simpler and quicker than their predecessors, our protocols also have slightly stronger security properties: in particular, they make no cryptographic use of s and so impose no subtle restrictions upon the use which is made of s by other protocols. A probabilistic model of information and retrieval: development and status Spärck Jones, K. Walker, S. Robertson, S.E. University of Cambridge, Computer Laboratory 1998-08 en Text UCAM-CL-TR-446 ISSN 1476-2986 The paper combines a comprehensive account of the probabilistic model of retrieval with new systematic experiments on TREC Programme material. It presents the model from its foundations through its logical development to cover more aspects of retrieval data and a wider range of system functions. Each step in the argument is matched by comparative retrieval tests, to provide a single coherent account of a major line of research. The experiments demonstrate, for a large test collection, that the probabilistic model is effective and robust, and that it responds appropriately, with major improvements in performance, to key features of retrieval situations. Are timestamps worth the effort? A formal treatment Bella, Giampaolo Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1998-09 en Text UCAM-CL-TR-447 ISSN 1476-2986 A computational interpretation of the λμ calculus Bierman, G.M. University of Cambridge, Computer Laboratory 1998-09 en Text UCAM-CL-TR-448 ISSN 1476-2986 Locales : A sectioning concept for Isabelle Kammüller, Florian Wenzel, Markus University of Cambridge, Computer Laboratory 1998-10 en Text UCAM-CL-TR-449 ISSN 1476-2986 Open service support for ATM van der Merwe, Jacobus Erasmus University of Cambridge, Computer Laboratory 1998-11 en Text UCAM-CL-TR-450 ISSN 1476-2986 The structure of open ATM control architectures Rooney, Sean University of Cambridge, Computer Laboratory 1998-11 en Text UCAM-CL-TR-451 ISSN 1476-2986 A formal proof of Sylow’s theorem : An experiment in abstract algebra with Isabelle Hol Kammüller, Florian Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1998-11 en Text UCAM-CL-TR-452 ISSN 1476-2986 The theorem of Sylow is proved in Isabelle HOL. We follow the proof by Wielandt that is more general than the original and uses a non-trivial combinatorial identity. The mathematical proof is explained in some detail leading on to the mechanization of group theory and the necessary combinatorics in Isabelle. We present the mechanization of the proof in detail giving reference to theorems contained in an appendix. Some weak points of the experiment with respect to a natural treatment of abstract algebraic reasoning give rise to a discussion of the use of module systems to represent abstract algebra in theorem provers. Drawing from that, we present tentative ideas for further research into a section concept for Isabelle. C formalised in HOL Norrish, Michael University of Cambridge, Computer Laboratory 1998-12 en Text UCAM-CL-TR-453 ISSN 1476-2986 We present a formal semantics of the C programming language, covering both the type system and the dynamic behaviour of programs. The semantics is wide-ranging, covering most of the language, with its most significant omission being the C library. Using a structural operational semantics we specify transition relations for C’s expressions, statements and declarations in higher order logic. The consistency of our definition is assured by its specification in the HOL theorem prover. With the theorem prover, we have used the semantics as the basis for a set of proofs of interesting theorems about C. We investigate properties of expressions and statements separately. In our chapter of results about expressions, we begin with two results about the interaction between the type system and the dynamic semantics. We have both type preservation, that the values produced by expressions conform to the type predicted for them; and type safety, that typed expressions will not block, but will either evaluate to a value, or cause undefined behaviour. We then also show that two broad classes of expression are deterministic. This last result is of considerable practical value as it makes later verification proofs significantly easier. In our chapter of results about statements, we prove a series of derived rules that provide C with Floyd-Hoare style “axiomatic” rules for verifying properties of programs. These rules are consequences of the original semantics, not independently stated axioms, so we can be sure of their soundness. This chapter also proves the correctness of an automatic tool for constructing post-conditions for loops with break and return statements. Finally, we perform some simple verification case studies, going some way towards demonstrating practical utility for the semantics and accompanying tools. This technical report is substantially the same as the PhD thesis I submitted in August 1998. The minor differences between that document and this are principally improvements suggested by my examiners Andy Gordon and Tom Melham, whom I thank for their help and careful reading. Parametric polymorphism and operational equivalence Pitts, Andrew M. University of Cambridge, Computer Laboratory 1998-12 en Text UCAM-CL-TR-454 ISSN 1476-2986 Multiple modalities Bierman, G.M. University of Cambridge, Computer Laboratory 1998-12 en Text UCAM-CL-TR-455 ISSN 1476-2986 An evaluation based approach to process calculi Ross, Joshua Robert Xavier University of Cambridge, Computer Laboratory 1999-01 en Text UCAM-CL-TR-456 ISSN 1476-2986 A concurrent object calculus: reduction and typing Gordon, Andrew D. Hankin, Paul D. University of Cambridge, Computer Laboratory 1999-02 en Text UCAM-CL-TR-457 ISSN 1476-2986 Final coalgebras as greatest fixed points in ZF set theory Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1999-03 en Text UCAM-CL-TR-458 ISSN 1476-2986 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, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint. Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are considered, as well as final coalgebras defined with respect to parameters. The disjoint sum construction is replaced by a smoother treatment of urelements that simplifies many of the derivations. The theory facilitates machine implementation of recursive definitions by letting both inductive and coinductive definitions be represented as fixedpoints. It has already been applied to the theorem prover Isabelle (Paulson, 1994). An open parallel architecture for data-intensive applications Afshar, Mohamad University of Cambridge, Computer Laboratory 1999-07 en Text UCAM-CL-TR-459 ISSN 1476-2986 Data-intensive applications consist of both declarative data-processing parts and imperative computational parts. For applications such as climate modelling, scale hits both the computational aspects which are typically handled in a procedural programming language, and the data-processing aspects which are handled in a database query language. Although parallelism has been successfully exploited in the data-processing parts by parallel evaluation of database queries associated with the application, current database query languages are poor at expressing the computational aspects, which are also subject to scale. This thesis proposes an open architecture that delivers parallelism shared between the database, system and application, thus enabling the integration of the conventionally separated query and non-query components of a data-intensive application. The architecture is data-model independent and can be used in a variety of different application areas including decision-support applications, which are query based, and complex applications, which comprise procedural language statements with embedded queries. The architecture encompasses a unified model of parallelism and the realisation of this model in the form of a language within which it is possible to describe both the query and non-query components of data-intensive applications. The language enables the construction of parallel applications by the hierarchical composition of platform-independent parallel forms, each of which implements a form of task or data parallelism. These forms may be used to determine both query and non-query actions. Queries are expressed in a declarative language based on “monoid comprehensions”. The approach of using monoids to model data types and monoid homomorphisms to iterate over collection types enables mathematically provable compile-time optimisations whilst also facilitating multiple collection types and data type extensibility. Monoid comprehension programs are automatically transformed into parallel programs composed of applications of the parallel forms, one of which is the “monoid homomorphism”. This process involves identifying the parts of a query where task and data parallelism are available and mapping that parallelism onto the most suitable form. Data parallelism in queries is mapped onto a form that implements combining tree parallelism for query evaluation and dividing tree parallelism to realise data partitioning. Task parallelism is mapped onto two separate forms that implement pipeline and independent parallelism. This translation process is applied to all comprehension queries including those in complex applications. The result is a skeleton program in which both the query and non-query parts are expressed within a single language. Expressions in this language are amenable to the application of optimising skeleton rewrite rules. A complete prototype of the decision-support architecture has been constructed on a 128-cell MIMD parallel computer. A demonstration of the utility of the query framework is performed by modelling some of OQL and a substantial subset of SQL. The system is evaluated for query speedup with a number of hardware configurations using a large music catalogue database. The results obtained show that the implementation delivers the performance gains expected while offering a convenient definition of the parallel environment. Message reception in the inductive approach Bella, Giampaolo University of Cambridge, Computer Laboratory 1999-03 en Text UCAM-CL-TR-460 ISSN 1476-2986 Integrating Gandalf and HOL Hurd, Joe University of Cambridge, Computer Laboratory 1999-03 en Text UCAM-CL-TR-461 ISSN 1476-2986 Gandalf is a first-order resolution theorem-prover, optimized for speed and specializing in manipulations of large clauses. In this paper I describe GANDALF TAC, a HOL tactic that proves goals by calling Gandalf and mirroring the resulting proofs in HOL. This call can occur over a network, and a Gandalf server may be set up servicing multiple HOL clients. In addition, the translation of the Gandalf proof into HOL fits in with the LCF model and guarantees logical consistency. Location-independent communication for mobile agents: a two-level architecture Sewell, Peter Wojciechowski, Paweł T. Pierce, Benjamin C. University of Cambridge, Computer Laboratory 1999-04 en Text UCAM-CL-TR-462 ISSN 1476-2986 Secure composition of insecure components Sewell, Peter Vitek, Jan University of Cambridge, Computer Laboratory 1999-04 en Text UCAM-CL-TR-463 ISSN 1476-2986 Feature representation for the automatic analysis of fluorescence in-situ hybridization images Lerner, Boaz Clocksin, William Dhanjal, Seema Hultén, Maj Bishop, Christipher University of Cambridge, Computer Laboratory 1999-05 en Text UCAM-CL-TR-464 ISSN 1476-2986 Gelfish – graphical environment for labelling FISH images Lerner, Boaz Dhanjal, Seema Hultén, Maj University of Cambridge, Computer Laboratory 1999-05 en Text UCAM-CL-TR-465 ISSN 1476-2986 Automatic signal classification in fluorescence in-situ hybridization images Lerner, Boaz Clocksin, William Dhanjal, Seema Hultén, Maj Bishop, Christipher University of Cambridge, Computer Laboratory 1999-05 en Text UCAM-CL-TR-466 ISSN 1476-2986 Mechanizing UNITY in Isabelle Paulson, Lawrence C. University of Cambridge, Computer Laboratory 1999-06 en Text UCAM-CL-TR-467 ISSN 1476-2986 UNITY is an abstract formalism for proving properties of concurrent systems, which typically are expressed using guarded assignments [Chandy and Misra 1988]. UNITY has been mechanized in higher-order logic using Isabelle, a proof assistant. Safety and progress primitives, their weak forms (for the substitution axiom) and the program composition operator (union) have been formalized. To give a feel for the concrete syntax, the paper presents a few extracts from the Isabelle definitions and proofs. It discusses a small example, two-process mutual exclusion. A mechanical theory of unions of programs supports a degree of compositional reasoning. Original work on extending program states is presented and then illustrated through a simple example involving an array of processes. Synthesis of asynchronous circuits Wilcox, Stephen Paul University of Cambridge, Computer Laboratory 1999-07 en Text UCAM-CL-TR-468 ISSN 1476-2986 A combination of geometry theorem proving and nonstandard analysis, with application to Newton’s Principia Fleuriot, Jacques Désiré University of Cambridge, Computer Laboratory 1999-08 en Text UCAM-CL-TR-469 ISSN 1476-2986 Modular reasoning in Isabelle Kammüller, Florian University of Cambridge, Computer Laboratory 1999-08 en Text UCAM-CL-TR-470 ISSN 1476-2986 Murphy’s law, the fitness of evolving species, and the limits of software reliability Brady, Robert M. Anderson, Ross J. Ball, Robin C. University of Cambridge, Computer Laboratory 1999-09 en Text UCAM-CL-TR-471 ISSN 1476-2986 We tackle two problems of interest to the software assurance community. Firstly, existing models of software development (such as the waterfall and spiral models) are oriented towards one-off software development projects, while the growth of mass market computing has led to a world in which most software consists of packages which follow an evolutionary development model. This leads us to ask whether anything interesting and useful may be said about evolutionary development. We answer in the affirmative. Secondly, existing reliability growth models emphasise the Poisson distribution of individual software bugs, while the empirically observed reliability growth for large systems is asymptotically slower than this. We provide a rigorous explanation of this phenomenon. Our reliability growth model is inspired by statistical thermodynamics, but also applies to biological evolution. It is in close agreement with experimental measurements of the fitness of an evolving species and the reliability of commercial software products. However, it shows that there are significant differences between the evolution of software and the evolution of species. In particular, we establish maximisation properties corresponding to Murphy’s law which work to the advantage of a biological species, but to the detriment of software reliability. Simulating music learning with autonomous listening agents: entropy, ambiguity and context Reis, Ben Y. University of Cambridge, Computer Laboratory 1999-09 en Text UCAM-CL-TR-472 ISSN 1476-2986 Computer algebra and theorem proving Ballarin, Clemens University of Cambridge, Computer Laboratory 1999-10 en Text UCAM-CL-TR-473 ISSN 1476-2986 A Bayesian methodology and probability density estimation for fluorescence in-situ hybridization signal classification Lerner, Boaz University of Cambridge, Computer Laboratory 1999-10 en Text UCAM-CL-TR-474 ISSN 1476-2986 A comparison of state-of-the-art classification techniques with application to cytogenetics Lerner, Boaz Lawrence, Neil D. University of Cambridge, Computer Laboratory 1999-10 en Text UCAM-CL-TR-475 ISSN 1476-2986 Linking ACL2 and HOL Staples, Mark University of Cambridge, Computer Laboratory 1999-11 en Text UCAM-CL-TR-476 ISSN 1476-2986 Presheaf models for CCS-like languages Cattani, Gian Luca Winskel, Glynn University of Cambridge, Computer Laboratory 1999-11 en Text UCAM-CL-TR-477 ISSN 1476-2986 Secure composition of untrusted code: wrappers and causality types Sewell, Peter Vitek, Jan University of Cambridge, Computer Laboratory 1999-11 en Text UCAM-CL-TR-478 ISSN 1476-2986 The interaction between fault tolerance and security Price, Geraint University of Cambridge, Computer Laboratory 1999-12 en Text UCAM-CL-TR-479 ISSN 1476-2986 This dissertation studies the effects on system design when including fault tolerance design principles within security services. We start by looking at the changes made to the trust model within protocol design, and how moving away from trusted server design principles affects the structure of the protocol. Taking the primary results from this work, we move on to study how control in protocol execution can be used to increase assurances in the actions of legitimate participants. We study some examples, defining two new classes of attack, and note that by increasing client control in areas of protocol execution, it is possible to overcome certain vulnerabilities. We then look at different models in fault tolerance, and how their adoption into a secure environment can change the design principles and assumptions made when applying the models. We next look at the application of timing checks in protocols. There are some classes of timing attack that are difficult to thwart using existing techniques, because of the inherent unreliability of networked communication. We develop a method of converting the Quality of Service mechanisms built into ATM networks in order to achieve another layer of protection against timing attacks. We then study the use of primary-backup mechanisms within server design, as previous work on server replication in security centres on the use of the state machine approach for replication, which provides a higher degree of assurance in system design, but adds complexity. We then provide a design for a server to reliably and securely store objects across a loosely coupled, distributed environment. The main goal behind this design was to realise the ability for a client to exert control over the fault tolerance inherent in the service. The main conclusions we draw from our research are that fault tolerance has a wider application within security than current practices, which are primarily based on replicating servers, and clients can exert control over the protocols and mechanisms to achieve resilience against differing classes of attack. We promote some new ideas on how, by challenging the prevailing model for client-server architectures in a secure environment, legitimate clients can have greater control over the services they use. We believe this to be a useful goal, given that the client stands to lose if the security of the server is undermined. Programming combinations of deduction and BDD-based symbolic calculation Gordon, Mike University of Cambridge, Computer Laboratory 1999-12 en Text UCAM-CL-TR-480 ISSN 1476-2986 Combining the Hol98 proof assistant with the BuDDy BDD package Gordon, Mike Larsen, Ken Friis University of Cambridge, Computer Laboratory 1999-12 en Text UCAM-CL-TR-481 ISSN 1476-2986 Biometric decision landscapes Daugman, John University of Cambridge, Computer Laboratory 2000-01 en Text UCAM-CL-TR-482 ISSN 1476-2986 This report investigates the “decision landscapes” that characterize several forms of biometric decision making. The issues discussed include: (i) Estimating the degrees-of-freedom associated with different biometrics, as a way of measuring the randomness and complexity (and therefore the uniqueness) of their templates. (ii) The consequences of combining more than one biometric test to arrive at a decision. (iii) The requirements for performing identification by large-scale exhaustive database search, as opposed to mere verification by comparison against a single template. (iv) Scenarios for Biometric Key Cryptography (the use of biometrics for encryption of messages). These issues are considered here in abstract form, but where appropriate, the particular example of iris recognition is used as an illustration. A unifying theme of all four sets of issues is the role of combinatorial complexity, and its measurement, in determining the potential decisiveness of biometric decision making. Elastic network control Bos, Hendrik Jaap University of Cambridge, Computer Laboratory 2000-01 en Text UCAM-CL-TR-483 ISSN 1476-2986 Automatic summarising and the CLASP system Tucker, Richard University of Cambridge, Computer Laboratory 2000-01 en Text UCAM-CL-TR-484 ISSN 1476-2986 This dissertation discusses summarisers and summarising in general, and presents CLASP, a new summarising system that uses a shallow semantic representation of the source text called a “predication cohesion graph”. Nodes in the graph are “simple predications” corresponding to events, states and entities mentioned in the text; edges indicate related or similar nodes. Summary content is chosen by selecting some of these predications according to criteria of “importance”, “representativeness” and “cohesiveness”. These criteria are expressed as functions on the nodes of a weighted graph. Summary text is produced either by extracting whole sentences from the source text, or by generating short, indicative “summary phrases” from the selected predications. CLASP uses linguistic processing but no domain knowledge, and therefore does not restrict the subject matter of the source text. It is intended to deal robustly with complex texts that it cannot analyse completely accurately or in full. Experiments in summarising stories from the Wall Street Journal suggest there may be a benefit in identifying important material in a semantic representation rather than a surface one, but that, despite the robustness of the source representation, inaccuracies in CLASP’s linguistic analysis can dramatically affect the readability of its summaries. I discuss ways in which this and other problems might be overcome. Three notes on the interpretation of Verilog Stewart, Daryl VanInwegen, Myra University of Cambridge, Computer Laboratory 2000-01 en Text UCAM-CL-TR-485 ISSN 1476-2986 Stretching a point: aspect and temporal discourse Thomas, James Richard University of Cambridge, Computer Laboratory 2000-02 en Text UCAM-CL-TR-486 ISSN 1476-2986 Sequential program composition in UNITY Vos, Tanja Swierstra, Doaitse University of Cambridge, Computer Laboratory 2000-03 en Text UCAM-CL-TR-487 ISSN 1476-2986 Formal verification of card-holder registration in SET Bella, Giampaolo Massacci, Fabio Paulson, Lawrence Tramontano, Piero University of Cambridge, Computer Laboratory 2000-03 en Text UCAM-CL-TR-488 ISSN 1476-2986 Designing a reliable publishing framework Lee, Jong-Hyeon University of Cambridge, Computer Laboratory 2000-04 en Text UCAM-CL-TR-489 ISSN 1476-2986 Due to the growth of the Internet and the widespread adoption of easy-to use web browsers, the web provides a new environment for conventional as well as new businesses. Publishing on the web is a fundamental and important means of supporting various activities on the Internet such as commercial transactions, personal home page publishing, medical information distribution, public key certification and academic scholarly publishing. Along with the dramatic growth of the web, the number of reported frauds is increasing sharply. Since the Internet was not originally designed for web publishing, it has some weaknesses that undermine its reliability. How can we rely on web publishing? In order to resolve this question, we need to examine what makes people confident when reading conventional publications printed on paper, to investigate what attacks can erode confidence in web publishing, and to understand the nature of publishing in general. In this dissertation, we examine security properties and policy models, and their applicability to publishing. We then investigate the nature of publishing so that we can extract its technical requirements. To help us understand the practical mechanisms which might satisfy these requirements, some applications of electronic publishing are discussed and some example mechanisms are presented. We conclude that guaranteed integrity, verifiable authenticity and persistent availability of publications are required to make web publishing more reliable. Hence we design a framework that can support these properties. To analyse the framework, we define a security policy for web publishing that focuses on the guaranteed integrity and authenticity of web publications, and then describe some technical primitives that enable us to achieve our requirements. Finally, the Jikzi publishing system—an implementation of our framework—is presented with descriptions of its architecture and possible applications. Selective mesh refinement for rendering Brown, Peter John Cameron University of Cambridge, Computer Laboratory 2000-04 en Text UCAM-CL-TR-490 ISSN 1476-2986 A key task in computer graphics is the rendering of complex models. As a result, there exist a large number of schemes for improving the speed of the rendering process, many of which involve displaying only a simplified version of a model. When such a simplification is generated selectively, i.e. detail is only removed in specific regions of a model, we term this selective mesh refinement. Selective mesh refinement can potentially produce a model approximation which can be displayed at greatly reduced cost while remaining perceptually equivalent to a rendering of the original. For this reason, the field of selective mesh refinement has been the subject of dramatically increased interest recently. The resulting selective refinement methods, though, are restricted in both the types of model which they can handle and the form of output meshes which they can generate. Our primary thesis is that a selectively refined mesh can be produced by combining fragments of approximations to a model without regard to the underlying approximation method. Thus we can utilise existing approximation techniques to produce selectively refined meshes in n-dimensions. This means that the capabilities and characteristics of standard approximation methods can be retained in our selectively refined models. We also show that a selectively refined approximation produced in this manner can be smoothly geometrically morphed into another selective refinement in order to satisfy modified refinement criteria. This geometric morphing is necessary to ensure that detail can be added and removed from models which are selectively refined with respect to their impact on the current view frustum. For example, if a model is selectively refined in this manner and the viewer approaches the model then more detail may have to be introduced to the displayed mesh in order to ensure that it satisfies the new refinement criteria. By geometrically morphing this introduction of detail we can ensure that the viewer is not distracted by “popping” artifacts. We have developed a novel framework within which these proposals have been verified. This framework consists of a generalised resolution-based model representation, a means of specifying refinement criteria and algorithms which can perform the selective refinement and geometric morphing tasks. The framework has allowed us to demonstrate that these twin tasks can be performed both on the output of existing approximation techniques and with respect to a variety of refinement criteria. A HTML version of this thesis is at http://www.cl.cam.ac.uk/research/rainbow/publications/pjcb/thesis/ Is hypothesis testing useful for subcategorization acquisition? Korhonen, Anna Gorrell, Genevive McCarthy, Diana University of Cambridge, Computer Laboratory 2000-05 en Text UCAM-CL-TR-491 ISSN 1476-2986 Nomadic Pict: language and infrastructure design for mobile computation Wojciechowski, Paweł Tomasz University of Cambridge, Computer Laboratory 2000-06 en Text UCAM-CL-TR-492 ISSN 1476-2986 Mobile agents – units of executing computation that can migrate between machines – are likely to become an important enabling technology for future distributed systems. We study the distributed infrastructures required for location-independent communication between migrating agents. These infrastructures are problematic: the choice or design of an infrastructure must be somewhat application-specific – any given algorithm will only have satisfactory performance for some range of migration and communication behaviour; the algorithms must be matched to the expected properties (and robustness demands) of applications and the failure characteristic of the communication medium. To study this problem we introduce an agent programming language – Nomadic Pict. It is designed to allow infrastructure algorithms to be expressed clearly, as translations from a high-level language to a lower level. The levels are based on rigorously-defined process calculi, which provide sharp levels of abstraction. In this dissertation we describe the language and use it to develop a distributed infrastructure for an example application. The language and examples have been implemented; we conclude with a description of the compiler and runtime system. Inductive verification of cryptographic protocols Bella, Giampaolo University of Cambridge, Computer Laboratory 2000-07 en Text UCAM-CL-TR-493 ISSN 1476-2986 The dissertation aims at tailoring Paulson’s Inductive Approach for the analysis of classical cryptographic protocols towards real-world protocols. The aim is pursued by extending the approach with new elements (e.g. timestamps and smart cards), new network events (e.g. message reception) and more expressive functions (e.g. agents’ knowledge). Hence, the aim is achieved by analysing large protocols (Kerberos IV and Shoup-Rubin), and by studying how to specify and verify their goals. More precisely, the modelling of timestamps and of a discrete time are first developed on BAN Kerberos, while comparing the outcomes with those of the BAN logic. The machinery is then applied to Kerberos IV, whose complicated use of session keys requires a dedicated treatment. Three new guarantees limiting the spy’s abilities in case of compromise of a specific session key are established. Also, it is discovered that Kerberos IV is subject to an attack due to the weak guarantees of confidentiality for the protocol responder. We develop general strategies to investigate the goals of authenticity, key distribution and non-injective agreement, which is a strong form of authentication. These strategies require formalising the agents’ knowledge of messages. Two approaches are implemented. If an agent creates a message, then he knows all components of the message, including the cryptographic key that encrypts it. Alternatively, a broad definition of agents’ knowledge can be developed if a new network event, message reception, is formalised. The concept of smart card as a secure device that can store long-term secrets and perform easy computations is introduced. The model cards can be stolen and/or cloned by the spy. The kernel of their built-in algorithm works correctly, so they spy cannot acquire unlimited knowledge from their use. However, their functional interface is unreliable, so they send correct outputs in an unspecified order. The provably secure protocol based on smart cards designed by Shoup & Rubin is mechanised. Some design weaknesses (unknown to the authors’ treatment by Bellare & Rogaway’s approach) are unveiled, while feasible corrections are suggested and verified. We realise that the evidence that a protocol achieves its goals must be available to the peers. In consequence, we develop a new a principle of prudent protocol design, goal availability, which holds of a protocol when suitable guarantees confirming its goals exist on assumptions that both peers can verify. Failure to observe our principle raises the risk of attacks, as is the case, for example, of the attack on Kerberos IV. An architecture for the notification, storage and retrieval of events Spiteri, Mark David University of Cambridge, Computer Laboratory 2000-07 en Text UCAM-CL-TR-494 ISSN 1476-2986 Automatic recognition of words in Arabic manuscripts Khorsheed, Mohammad S.M. University of Cambridge, Computer Laboratory 2000-07 en Text UCAM-CL-TR-495 ISSN 1476-2986 The need to transliterate large numbers of historic Arabic documents into machine-readable form has motivated new work on offline recognition of Arabic script. Arabic script presents two challenges: orthography is cursive and letter shape is context sensitive. This dissertation presents two techniques to achieve high word recognition rates: the segmentation-free technique and the segmentation-based technique. The segmentation-free technique treats the word as a whole. The word image is first transformed into a normalised polar image. The two-dimensional Fourier transform is then applied to the polar image. This results in a Fourier spectrum that is invariant to dilation, translation, and rotation. The Fourier spectrum is used to form the word template, or train the word model in the template-based and the multiple hidden Markov model (HMM) recognition systems, respectively. The recognition of an input word image is based on the minimum distance measure from the word templates and the maximum likelihood probability for the word models. The segmentation-based technique uses a single hidden Markov model, which is composed of multiple character-models. The technique implements the analytic approach in which words are segmented into smaller units, not necessarily characters. The word skeleton is decomposed into a number of links in orthographic order, it is then transferred into a sequence of discrete symbols using vector quantisation. the training of each character-model is performed using either: state assignment in the lexicon-driven configuration or the Baum-Welch method in the lexicon-free configuration. The observation sequence of the input word is given to the hidden Markov model and the Viterbi algorithm is applied to provide an ordered list of the candidate recognitions. Contexts and embeddings for closed shallow action graphs Cattani, Gian Luca Leifer, James J. Milner, Robin University of Cambridge, Computer Laboratory 2000-07 en Text UCAM-CL-TR-496 ISSN 1476-2986 Towards a formal type system for ODMG OQL Bierman, G.M. Trigoni, A. University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-497 ISSN 1476-2986 Applied π – a brief tutorial Sewell, Peter University of Cambridge, Computer Laboratory 2000-07 en Text UCAM-CL-TR-498 ISSN 1476-2986 This note provides a brief introduction to π-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple π-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed π-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5). Enhancing spatial deformation for virtual sculpting Gain, James Edward University of Cambridge, Computer Laboratory 2000-08 en Text UCAM-CL-TR-499 ISSN 1476-2986 The task of computer-based free-form shape design is fraught with practical and conceptual difficulties. Incorporating elements of traditional clay sculpting has long been recognised as a means of shielding a user from the complexities inherent in this form of modelling. The premise is to deform a mathematically-defined solid in a fashion that loosely simulates the physical moulding of an inelastic substance, such as modelling clay or silicone putty. Virtual sculpting combines this emulation of clay sculpting with interactive feedback. Spatial deformations are a class of powerful modelling techniques well suited to virtual sculpting. They indirectly reshape an object by warping the surrounding space. This is analogous to embedding a flexible shape within a lump of jelly and then causing distortions by flexing the jelly. The user controls spatial deformations by manipulating points, curves or a volumetric hyperpatch. Directly Manipulated Free-Form Deformation (DMFFD), in particular, merges the hyperpatch- and point-based approaches and allows the user to pick and drag object points directly. This thesis embodies four enhancements to the versatility and validity of spatial deformation: 1. We enable users to specify deformations by manipulating the normal vector and tangent plane at a point. A first derivative frame can be tilted, twisted and scaled to cause a corresponding distortion in both the ambient space and inset object. This enhanced control is accomplished by extending previous work on bivariate surfaces to trivariate hyperpatches. 2. We extend DMFFD to enable curve manipulation by exploiting functional composition and degree reduction. Although the resulting curve-composed DMFFD introduces some modest and bounded approximation, it is superior to previous curve-based schemes in other respects. Our technique combines all three forms of spatial deformation (hyperpatch, point and curve), can maintain any desired degree of derivative continuity, is amenable to the automatic detection and prevention of self-intersection, and achieves interactive update rates over the entire deformation cycle. 3. The approximation quality of a polygon-mesh object frequently degrades under spatial deformation to become either oversaturated or undersaturated with polygons. We have devised an efficient adaptive mesh refinement and decimation scheme. Our novel contributions include: incorporating fully symmetrical decimation, reducing the computation cost of the refinement/decimation trigger, catering for boundary and crease edges, and dealing with sampling problems. 4. The potential self-intersection of an object is a serious weakness in spatial deformation. We have developed a variant of DMFFD which guards against self-intersection by subdividing manipulations into injective (one-to-one) mappings. This depends on three novel contributions: analytic conditions for identifying self-intersection, and two injectivity tests (one exact but computationally costly and the other approximate but efficient). The memorability and security of passwords – some empirical results Yan, Jianxin Blackwell, Alan Anderson, Ross Grant, Alasdair University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-500 ISSN 1476-2986 There are many things that are ‘well known’ about passwords, such as that uers can’t remember strong passwords and that the passwords they can remember are easy to guess. However, there seems to be a distinct lack of research on the subject that would pass muster by the standards of applied psychology. Here we report a controlled trial in which, of four sample groups of about 100 first-year students, three were recruited to a formal experiment and of these two were given specific advice about password selection. The incidence of weak passwords was determined by cracking the password file, and the number of password resets was measured from system logs. We observed a number of phenomena which run counter to the established wisdom. For example, passwords based on mnemonic phrases are just as hard to crack as random passwords yet just as easy to remember as naive user selections. Integrated quality of service management Ingram, David University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-501 ISSN 1476-2986 Formalizing basic number theory Rasmussen, Thomas Marthedal University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-502 ISSN 1476-2986 Hardware/software co-design using functional languages Mycroft, Alan Sharp, Richard University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-503 ISSN 1476-2986 In previous work we have developed and prototyped a silicon compiler which translates a functional language (SAFL) into hardware. Here we present a SAFL-level program transformation which: (i) partitions a specification into hardware and software parts and (ii) generates a specialised architecture to execute the software part. The architecture consists of a number of interconnected heterogeneous processors. Our method allows a large design space to be explored by systematically transforming a single SAFL specification to investigate different points on the area-time spectrum. Word sense selection in texts: an integrated model Kwong, Oi Yee University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-504 ISSN 1476-2986 Early systems for word sense disambiguation (WSD) often depended on individual tailor-made lexical resources, hand-coded with as much lexical information as needed, but of severely limited vocabulary size. Recent studies tend to extract lexical information from a variety of existing resources (e.g. machine-readable dictionaries, corpora) for broad coverage. However, this raises the issue of how to combine the information from different resources. Thus while different types of resource could make different contribution to WSD, studies to date have not shown what contribution they make, how they should be combined, and whether they are equally relevant to all words to be disambiguated. This thesis proposes an Integrated Model as a framework to study the inter-relatedness of three major parameters in WSD: Lexical Resource, Contextual Information, and Nature of Target Words. We argue that it is their interaction which shapes the effectiveness of any WSD system. A generalised, structurally-based sense-mapping algorithm was designed to combine various types of lexical resource. This enables information from these resources to be used simultaneously and compatibly, while respecting their distinctive structures. In studying the effect of context on WSD, different semantic relations available from the combined resources were used, and a recursive filtering algorithm was designed to overcome combinatorial explosion. We then investigated, from two directions, how the target words themselves could affect the usefulness of different types of knowledge. In particular, we modelled WSD with the cloze test format, i.e. as texts with blanks and all senses for one specific word as alternative choices for filling the blank. A full-scale combination of WordNet and Roget’s Thesaurus was done, linking more than 30,000 senses. Using these two resources in combination, a range of disambiguation tests was done on more than 60,000 noun instances from corpus texts of different types, and 60 blanks from real cloze texts. Results show that combining resources is useful for enriching lexical information, and hence making WSD more effective though not completely. Also, different target words make different demand on contextual information, and this interaction is closely related to text types. Future work is suggested for expanding the analysis on target nature and making the combination of disambiguation evidence sensitive to the requirements of the word being disambiguated. Models for name-passing processes: interleaving and causal Cattani, Gian Luca Sewell, Peter University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-505 ISSN 1476-2986 We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For noninterleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi. Modules, abstract types, and distributed versioning Sewell, Peter University of Cambridge, Computer Laboratory 2000-09 en Text UCAM-CL-TR-506 ISSN 1476-2986 In a wide-area distributed system it is often impractical to synchronise software updates, so one must deal with many coexisting versions. We study static typing support for modular wide-area programming, modelling separate compilation/linking and execution of programs that interact along typed channels. Interaction may involve communication of values of abstract types; we provide the developer with fine-grain versioning control of these types to support interoperation of old and new code. The system makes use of a second-class module system with singleton kinds; we give a novel operational semantics for separate compilation/linking and execution and prove soundness. Mechanizing a theory of program composition for UNITY Paulson, Lawrence University of Cambridge, Computer Laboratory 2000-11 en Text UCAM-CL-TR-507 ISSN 1476-2986 Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which Charpentier and Chandy [1999] have illustrated by developing a large example in the UNITY formalism. The present paper describes extensive experiments on mechanizing the compositionality theory and the example, using the proof tool Isabelle. Broader issues are discussed, in particular, the formalization of program states. The usual representation based upon maps from variables to values is contrasted with the alternatives, such as a signature of typed variables. Properties need to be transferred from one program component’s signature to the common signature of the system. Safety properties can be so transferred, but progress properties cannot be. Using polymorphism, this problem can be circumvented by making signatures sufficiently flexible. Finally the proof of the example itself is outlined. Shallow linear action graphs and their embeddings Leifer, James Milner, Robin University of Cambridge, Computer Laboratory 2000-10 en Text UCAM-CL-TR-508 ISSN 1476-2986 Proximity visualisation of abstract data Basalaj, Wojciech University of Cambridge, Computer Laboratory 2001-01 en Text UCAM-CL-TR-509 ISSN 1476-2986 Data visualisation is an established technique for exploration, analysis and presentation of data. A graphical presentation is generated from the data content, and viewed by an observer, engaging vision – the human sense with the greatest bandwidth, and the ability to recognise patterns subconciously. For instance, a correlation present between two variables can be elucidated with a scatter plot. An effective visualisation can be difficult to achieve for an abstract collection of objects, e.g. a database table with many attributes, or a set of multimedia documents, since there is no immediately obvious way of arranging the objects based on their content. Thankfully, similarity between pairs of elements of such a collection can be measured, and a good overview picture should respect this proximity information, by positioning similar elements close to one another, and far from dissimilar objects. The resulting proximity visualisation is a topology preserving map of the underlying data collection, and this work investigates various methods for generating such maps. A number of algorithms are devised, evaluated quantitatively by means of statistical inference, and qualitatively in a case study for each type of data collection. Other graphical representations for abstract data are surveyed and compared to proximity visualisation. A standard method for modelling prximity relations is multidimensional scaling (MDS) analysis. The result is usually a two- or three-dimensional configuration of points – each representing a single element from a collection., with inter-point distances approximating the corresponding proximities. The quality of this approximation can be expressed as a loss function, and the optimal arrangement can be found by minimising it numerically – a procedure known as least-squares metric MDS. This work presents a number of algorithmic instances of this problem, using established function optimisation heuristics: Newton-Raphson, Tabu Search, Genetic Algorithm, Iterative Majorization, and Stimulated annealing. Their effectiveness at minimising the loss function is measured for a representative sample of data collections, and the relative ranking established. The popular classical scaling method serves as a benchmark for this study. The computational cost of conventional MDS makes it unsuitable for visualising a large data collection. Incremental multidimensional scaling solves this problem by considering only a carefully chosen subset of all pairwise proximities. Elements that make up cluster diameters at a certain level of the single link cluster hierarchy are identified, and are subject to standard MDS, in order to establish the overall shape of the configuration. The remaining elements are positioned independently of one another with respect to this skeleton configuration. For very large collections the skeleton configuration can itself be built up incrementally. The incremental method is analysed for the compromise between solution quality and the proportion of proximities used, and compared to Principal Components Analysis on a number of large database tables. In some applications it is convenient to represent individual objects by compact icons of fixed size, for example the use of thumbnails when visualising a set of images. Because the MDS analysis only takes the position of icons into account, and not their size, its direct use for visualisation may lead to partial or complete overlap of icons. Proximity grid – an analogue of MDS in a discrete domain – is proposed to overcome this deficiency. Each element of an abstract data collection is represented within a single cell of the grid, and thus considerable detail can be shown without overlap. The proximity relationships are preserved by clustering similar elements in the grid, and keeping dissimilar ones apart. Algorithms for generating such an arrangement are presented and compared in terms of output quality to one another as well as standard MDS. Switchlets and resource-assured MPLS networks Mortier, Richard Isaacs, Rebecca Fraser, Keir University of Cambridge, Computer Laboratory 2000-05 en Text UCAM-CL-TR-510 ISSN 1476-2986 MPLS (Multi-Protocol Label Switching) is a technology with the potential to support multiple control systems, each with guaranteed QoS (Quality of Service), on connectionless best-effort networks. However, it does not provide all the capabilities required of a multi-service network. In particular, although resource-assured VPNs (Virtual Private Networks) can be created, there is no provision for inter-VPN resource management. Control flexibility is limited because resources must be pinned down to be guaranteed, and best-effort flows in different VPNs compete for the same resources, leading to QoS crosstalk. The contribution of this paper is an implementation on MPLS of a network control framework that supports inter-VPN resource management. Using resource partitions known as switchlets, it allows the creation of multiple VPNs with guaranteed resource allocations, and maintains isolation between these VPNs. Devolved control techniques permit each VPN a customised control system. We motivate our work by discussing related efforts and example scenarios of effective deployment of our system. The implementation is described and evaluated, and we address interoperability with external IP control systems, in addition to interoperability of data across different layer 2 technologies. Software visualization in Prolog Grant, Calum University of Cambridge, Computer Laboratory 1999-12 en Text UCAM-CL-TR-511 ISSN 1476-2986 Software visualization (SV) uses computer graphics to communicate the structure and behaviour of complex software and algorithms. One of the important issues in this field is how to specify SV, because existing systems are very cumbersome to specify and implement, which limits their effectiveness and hinders SV from being integrated into professional software development tools. In this dissertation the visualization process is decomposed into a series of formal mappings, which provides a formal foundation, and allows separate aspects of visualization to be specified independently. The first mapping specifies the information content of each view. The second mapping specifies a graphical representation of the information, and a third mapping specifies the graphical components that make up the graphical representation. By combining different mappings, completely different views can be generated. The approach has been implemented in Prolog to provide a very high level specification language for information visualization, and a knowledge engineering environment that allows data queries to tailor the information in a view. The output is generated by a graphical constraint solver that assembles the graphical components into a scene. This system provides a framework for SV called Vmax. Source code and run-time data are analyzed by Prolog to provide access to information about the program structure and run-time data for a wide range of highly interconnected browsable views. Different views and means of visualization can be selected from menus. An automatic legend describes each view, and can be interactively modified to customize how data is presented. A text window for editing source code is synchronized with the graphical view. Vmax is a complete Java development environment and end user SV system. Vmax compares favourably to existing SV systems in many taxonometric criteria, including automation, scope, information content, graphical output form, specification, tailorability, navigation, granularity and elision control. The performance and scalability of the new approach is very reasonable. We conclude that Prolog provides a formal and high level specification language that is suitable for specifying all aspects of a SV system. An algebraic framework for modelling and verifying microprocessors using HOL Fox, Anthony University of Cambridge, Computer Laboratory 2001-03 en Text UCAM-CL-TR-512 ISSN 1476-2986 This report describes an algebraic approach to the specification and verification of microprocessor designs. Key results are expressed and verified using the HOL proof tool. Particular attention is paid to the models of time and temporal abstraction, culminating in a number of one-step theorems. This work is then explained with a small but complete case study, which verifies the correctness of a datapath with microprogram control. Generic summaries for indexing in information retrieval – Detailed test results Sakai, Tetsuya Spärck Jones, Karen University of Cambridge, Computer Laboratory 2001-05 en Text UCAM-CL-TR-513 ISSN 1476-2986 This paper examines the use of generic summaries for indexing in information retrieval. Our main observations are that: – With or without pseudo-relevance feedback, a summary index may be as effective as the corresponding fulltext index for precision-oriented search of highly relevant documents. But a reasonably sophisticated summarizer, using a compression ratio of 10–30%, is desirable for this purpose. – In pseudo-relevance feedback, using a summary index at initial search and a fulltext index at final search is possibly effective for precision-oriented search, regardless of relevance levels. This strategy is significantly more effective than the one using the summary index only and probably more effective than using summaries as mere term selection filters. For this strategy, the summary quality is probably not a critical factor, and a compression ratio of 5–10% appears best. Nomadic π-calculi: Expressing and verifying communication infrastructure for mobile computation Unyapoth, Asis University of Cambridge, Computer Laboratory 2001-06 en Text UCAM-CL-TR-514 ISSN 1476-2986 This thesis addresses the problem of verifying distributed infrastructure for mobile computation. In particular, we study language primitives for communication between mobile agents. They can be classified into two groups. At a low level there are “location dependent” primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are “location independent” primitives that allow communication with a mobile agent irrespective of any migrations. Implementation of the high level requires delicate distributed infrastructure algorithms. In earlier work of Sewell, Wojciechowski and Pierce, the two levels were made precise as process calculi, allowing such algorithms to be expressed as encodings of the high level into the low level; a distributed programming language “Nomadic Pict” has been built for experimenting with such encodings. This thesis turns to semantics, giving a definition of the core language (with a type system) and proving correctness of an example infrastructure. This involves extending the standard semantics and proof techniques of process calculi to deal with the new notions of sites and agents. The techniques adopted include labelled transition semantics, operational equivalences and preorders (e.g., expansion and coupled simulation), “up to” equivalences, and uniform receptiveness. We also develop two novel proof techniques for capturing the design intuitions regarding mobile agents: we consider “translocating” versions of operational equivalences that take migration into account, allowing compositional reasoning; and “temporary immobility”, which captures the intuition that while an agent is waiting for a lock somewhere in the system, it will not migrate. The correctness proof of an example infrastructure is non-trivial. It involves analysing the possible reachable states of the encoding applied to an arbitrary high-level source program. We introduce an intermediate language for factoring out as many ‘house-keeping’ reduction steps as possible, and focusing on the partially-committed steps. The UDP calculus: rigorous semantics for real networking Serjantov, Andrei Sewell, Peter Wansbrough, Keith University of Cambridge, Computer Laboratory 2001-07 en Text UCAM-CL-TR-515 ISSN 1476-2986 Dynamic provisioning of resource-assured and programmable virtual private networks Isaacs, Rebecca University of Cambridge, Computer Laboratory 2001-09 en Text UCAM-CL-TR-516 ISSN 1476-2986 Virtual Private Networks (VPNs) provide dedicated connectivity to a closed group of users on a shared network. VPNs have traditionally been deployed for reasons of economy of scale, but have either been statically defined, requiring manual configuration, or else unable to offer any quality of service (QoS) guarantees. This dissertation describes VServ, a service offering dynamic and resource-assured VPNs that can be acquired and modified on demand. In VServ, a VPN is both a subset of physical resources, such as bandwidth and label space, together with the means to perform fine-grained management of those resources. This network programmability, combined with QoS guarantees, enables the multiservice network – a single universal network that can support all types of service and thus be efficient, cost-effective and flexible. VServ is deployed over a network control framework known as Tempest. The Tempest explicitly distinguishes between inter- and intra-VPN resource management mechanisms. This makes the dynamic resource reallocation capabilities of VServ viable, whilst handling highly dynamic VPNs or a large number of VPNs. Extensions to the original implementation of the Tempest to support dynamically reconfigurable QoS are detailed. A key part of a dynamic and responsive VPN service is fully automated VPN provisioning. A notation for VPN specification is described, together with mechanisms for incorporating policies of the service provider and the current resource availability in the network into the design process. The search for a suitable VPN topology can be expressed as a optimisation problem that is not computationally tractable except for very small networks. This dissertation describes how the search is made practical by tailoring it according to the characteristics of the desired VPN. Availability of VServ is addressed with a proposal for distributed VPN creation. A resource revocation protocol exploits the dynamic resource management capabilities of VServ to allow adaptation in the control plane on a per-VPN basis. Managed resource revocation supports highly flexible resource allocation and reallocation policies, allowing VServ to efficiently provision for short-lived or highly dynamic VPNs. The Cambridge Multimedia Document Retrieval Project: summary of experiments Spärck Jones, Karen Jourlin, P. Johnson, S.E. Woodland, P.C. University of Cambridge, Computer Laboratory 2001-07 en Text UCAM-CL-TR-517 ISSN 1476-2986 This report summarises the experimental work done under the Multimedia Document Retrieval (MDR) project at Cambridge from 1997-2000, with selected illustrations. The focus is primarily on retrieval studies, and on speech tests directly related to retrieval, not on speech recognition itself. The report draws on the many and varied tests done during the project, but also presents a new series of results designed to compare strategies across as many different data sets as possible by using consistent system parameter settings. The project tests demonstrate that retrieval from files of audio news material transcribed using a state of the art speech recognition system can match the reference level defined by human transcriptions; and that expansion techniques, especially when applied to queries, can be very effective means for improving basic search performance. An attack on a traitor tracing scheme Yan, Jeff Jianxin Wu, Yongdong University of Cambridge, Computer Laboratory 2001-07 en Text UCAM-CL-TR-518 ISSN 1476-2986 In Crypto’99, Boneh and Franklin proposed a public key traitor tracing scheme, which was believed to be able to catch all traitors while not accusing any innocent users (i.e., full-tracing and error-free). Assuming that Decision Diffie-Hellman problem is unsolvable in Gq, Boneh and Franklin proved that a decoder cannot distinguish valid ciphertexts from invalid ones that are used for tracing. However, our novel pirate decoder P3 manages to make some invalid ciphertexts distinguishable without violating their assumption, and it can also frame innocent user coalitions to fool the tracer. Neither the single-key nor arbitrary pirate tracing algorithm presented in [1] can identify all keys used by P3 as claimed. Instead, it is possible for both algorithms to catch none of the traitors. We believe that the construction of our novel pirate also demonstrates a simple way to defeat some other black-box traitor tracing schemes in general. Local evidence in document retrieval Choquette, Martin University of Cambridge, Computer Laboratory 2001-08 en Text UCAM-CL-TR-519 ISSN 1476-2986 Ternary and three-point univariate subdivision schemes Hassan, Mohamed Dodgson, Neil A. University of Cambridge, Computer Laboratory 2001-09 en Text UCAM-CL-TR-520 ISSN 1476-2986 The generating function formalism is used to analyze the continuity properties of univariate ternary subdivision schemes. These are compared with their binary counterparts. Operational congruences for reactive systems Leifer, James University of Cambridge, Computer Laboratory 2001-09 en Text UCAM-CL-TR-521 ISSN 1476-2986 Practical behavioural animation based on vision and attention Gillies, Mark F.P. University of Cambridge, Computer Laboratory 2001-09 en Text UCAM-CL-TR-522 ISSN 1476-2986 The animation of human like characters is a vital aspect of computer animation. Most animations rely heavily on characters of some sort or other. This means that one important aspect of computer animation research is to improve the animation of these characters both by making it easier to produce animations and by improving the quality of animation produced. One approach to animating characters is to produce a simulation of the behaviour of the characters which will automatically animate the character. The dissertation investigates the simulation of behaviour in practical applications. In particular it focuses on models of visual perception for use in simulating human behaviour. A simulation of perception is vital for any character that interacts with its surroundings. Two main aspects of the simulation of perception are investigated: – The use of psychology for designing visual algorithms. – The simulation of attention in order to produce both behaviour and gaze patterns. Psychological theories are a useful starting point for designing algorithms for simulating visual perception. The dissertation investigates their use and presents some algorithms based on psychological theories. Attention is the focusing of a person’s perception on a particular object. The dissertation presents a simulation of what a character is attending to (looking at). This is used to simulate behaviour and for animating eye movements. The algorithms for the simulation of vision and attention are applied to two tasks in the simulation of behaviour. The first is a method for designing generic behaviour patterns from simple pieces of motion. The second is a behaviour pattern for navigating a cluttered environment. The simulation of vision and attention gives advantages over existing work on both problems. The approaches to the simulation of perception will be evaluated in the context of these examples. Bigraphical reactive systems: basic theory Milner, Robin University of Cambridge, Computer Laboratory 2001-09 en Text UCAM-CL-TR-523 ISSN 1476-2986 A notion of bigraph is proposed as the basis for a model of mobile interaction. A bigraph consists of two independent structures: a topograph representing locality and a monograph representing connectivity. Bigraphs are equipped with reaction rules to form bigraphical reactive systems (BRSs), which include versions of the π-calculus and the ambient calculus. Bigraphs are shown to be a special case of a more abstract notion, wide reactive systems (WRSs), not assuming any particular graphical or other structure but equipped with a notion of width, which expresses that agents, contexts and reactions may all be widely distributed entities. A behavioural theory is established for WRSs using the categorical notion of relative pushout; it allows labelled transition systems to be derived uniformly, in such a way that familiar behavioural preorders and equivalences, in particular bisimilarity, are congruential under certain conditions. Then the theory of bigraphs is developed, and they are shown to meet these conditions. It is shown that, using certain functors, other WRSs which meet the conditions may also be derived; these may, for example, be forms of BRS with additional structure. Simple examples of bigraphical systems are discussed; the theory is developed in a number of ways in preparation for deeper application studies. Verifying the SET purchase protocols Bella, Giampaolo Massacci, Fabio Paulson, Lawrence C. University of Cambridge, Computer Laboratory 2001-11 en Text UCAM-CL-TR-524 ISSN 1476-2986 The Secure Electronic Transaction (SET) protocol has been proposed by a consortium of credit card companies and software corporations to guarantee the authenticity of e-commerce transactions and the confidentiality of data. When the customer makes a purchase, the SET dual signature keeps his account details secret from the merchant and his choice of goods secret from the bank. This paper reports verification results for the purchase step of SET, using the inductive method. The credit card details do remain confidential. The customer, merchant and bank can confirm most details of a transaction even when some of those details are kept from them. The usage of dual signatures requires repetition in protocol messages, making proofs more difficult but still feasible. The formal analysis has revealed a significant defect. The dual signature lacks explicitness, giving rise to potential vulnerabilities. Extensible virtual machines Harris, Timothy L. University of Cambridge, Computer Laboratory 2001-12 en Text UCAM-CL-TR-525 ISSN 1476-2986 Virtual machines (VMs) have enjoyed a resurgence as a way of allowing the same application program to be used across a range of computer systems. This flexibility comes from the abstraction that the provides over the native interface of a particular computer. However, this also means that the application is prevented from taking the features of particular physical machines into account in its implementation. This dissertation addresses the question of why, where and how it is useful, possible and practicable to provide an application with access to lower-level interfaces. It argues that many aspects of implementation can be devolved safely to untrusted applications and demonstrates this through a prototype which allows control over run-time compilation, object placement within the heap and thread scheduling. The proposed architecture separates these application-specific policy implementations from the application itself. This allows one application to be used with different policies on different systems and also allows naïve or premature optimizations to be removed. Extending lossless image compression Penrose, Andrew J. University of Cambridge, Computer Laboratory 2001-12 en Text UCAM-CL-TR-526 ISSN 1476-2986 “It is my thesis that worthwhile improvements can be made to lossless image compression schemes, by considering the correlations between the spectral, temporal and interview aspects of image data, in extension to the spatial correlations that are traditionally exploited.” Images are an important part of today’s digital world. However, due to the large quantity of data needed to represent modern imagery the storage of such data can be expensive. Thus, work on efficient image storage (image compression) has the potential to reduce storage costs and enable new applications. Many image compression schemes are lossy; that is they sacrifice image informationto achieve very compact storage. Although this is acceptable for many applications, some environments require that compression not alter the image data. This lossless image compression has uses in medical, scientific and professional video processing applications. Most of the work on lossless image compression has focused on monochrome images and has made use of the spatial smoothness of image data. Only recently have researchers begun to look specifically at the lossless compression of colour images and video. By extending compression schemes for colour images and video, the storage requirements for these important classes of image data can be further reduced. Much of the previous research into lossless colour image and video compression has been exploratory. This dissertation studies the