Browse

ftp://ftp.cl.cam.ac.uk (64)

	ftp://ftp.cl.cam.ac.uk/papers/reports/TR228-mdh-dm-dan.ps.Z, 19910712 The Desk Area Network Mark Hayter and Derek McAuley University of Cambridge Computer Laboratory May 1991 To appear in ACM Operating Systems Review
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR250-iaf-touringmachines.ps.Z, 19920519 TouringMachines: Autonomous Agents with Attitudes Innes A. Fergusony Computer Laboratory, University of Cambridge New Museums Site, Cambridge CB2 3QG England, UK. Internet: iaf@cl.cam.ac.uk Technical Report 250 { April 1992
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR277-bdp-chess-like.ps.gz, 19921125 An earlier version of this paper appears in: H.J. van den Herik and L.V. Allis, editors, Heuristic Programming in Artificial Intelligence 3 { The Third Computer Olympiad. Ellis Horwood, 1992. METAGAME in Symmetric Chess-Like Games Barney Pell1 University of Cambridge Cambridge, UK E-mail:
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR276-bdp-metagame.ps.gz, 19921125 An earlier version of this paper appears in: H.J. van den Herik and L.V. Allis, editors, Heuristic Programming in Artificial Intelligence 3 { The Third Computer Olympiad. Ellis Horwood, 1992. METAGAME: A New Challenge for Games and Learning Barney Pell1 University of Cambridge Cambridge, UK E-mail:
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR275-bdp-go.ps.gz, 19921125 In D.N.L. Levy and D.F. Beal, editors, Heuristic Programming in Artificial Intelligence 2 { The Second Computer Olympiad. Ellis Horwood, 1991. Exploratory Learning in the Game of GO Barney Pell1 University of Cambridge Cambridge UK E-mail: bdp@cl.cam.ac.uk
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR298-jmsd-thesis.ps.gz, 19930414 Multicast in the Asynchronous Transfer Mode Environment John Matthew Simon Doar St. John's College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy January 1993
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR299-bdp-bridge.ps.gz, 19930424 Gamb ack, Rayner & Pell: Pragmatic Reasoning in Bridge 23 Searle, J.R. 1979. Expression and Meaning Studies in the Theory of Speech Acts. Cambridge, England: Cambridge University Press. Stanier, A. 1975. Bribip: A Bridge-Bidding Program . the 4th International Joint
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR292-cjs-synchronisation.ps.Z, 19930429 Synchronisation Services for Digital Continuous Media Cormac John Sreenan Christ's College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy October 1992
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR302-bdp-lpar.ps.gz, 19930528 In Proceedings of the Workshop on Knowledge Compilation and Speedup Learning, at Machine Learning Conference, Amherst, Mass., 1993. Logic Programming for General Game-Playing Barney Pell1 Computer Laboratory University of Cambridge Cambridge, CB2 3QG, UK E-mail: bdp@cl.cam.ac.uk
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR268-pwj-cmfileserver.ps.Z, 19931115 Network File Server Design for Continuous Media Paul Wenceslas Jardetzky Darwin College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy August 1992 Summary Significant effort is currently being applied to the integration of diverse digital communication services
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR319-mdh-DAN-architecture.ps.gz, 19931115 A Workstation Architecture to Support Multimedia Mark David Hayter St John's College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy September 1993
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR318-jg-program-refinement.ps.gz, 19931122 A Method of Program Refinement Jim Grundy Fitzwilliam College A dissertation submitted for the degree of Doctor of Philosophy in the University of Cambridge November 1993 Copyright c Jim Grundy 1993 All rights reserved. This work is copyright and may not be reproduced, stored nor distributed in whole or
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR319-mdh-DAN-architecture.grayscale.ps.gz, 19931123 A Workstation Architecture to Support Multimedia Mark David Hayter St John's College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy September 1993
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR321-ap-relational-properties-of-domains.ps.gz, 19931202 Relational Properties of Domains Andrew M. Pittsy Cambridge University Computer Laboratory, Cambridge, England
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR304-lcp-coinduction-fig.ps.Z, 19931213 Pure Isabelle IFOL CTT HOL LK ZF LCF Modal logics FOL 1 x x n 1 x 1 1 xn 1 x 1 1 n x2 x2 x2 x 1 1 n x2 x2 x2 x 1 1 n x2 x2 x2 Diagram 1. Isabelle's object-logics Diagram 2. Infinite binary tree Diagram 3. Infinite-branching tree
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR186-dm-thesis.ps.gz, 19940110 Protocol Design for High Speed Networks Derek Robert McAuley Fitzwilliam College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy September 1989 Preface Except where otherwise stated in the text, this dissertation is the result of my own work and is not the outcome
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR291-ksj-jrg-evaluating-nl-systems.ps.gz, 19940211 This is a mandatory blank page 1 E V A L U A T I N G N A T U R A L L A N G U A G E P R O C E S S I N G S Y S T E M S J R Galliers and K Sparck Jones Computer Laboratory, University of Cambridge New Museums Site, Pembroke Street, Cambridge CB2 3QG, England Technical Report 291 March 1993
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR273-iaf-thesis.ps.gz, 19940323 TouringMachines: An Architecture for Dynamic, Rational, Mobile Agents Innes Andrew Ferguson Clare Hall A dissertation submitted for the degree of Doctor of Philosophy in the University of Cambridge October 1992 Summary The computer-controlled operating environments at such facilities as automated
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR341-job-support-multimedia-applications.ps.gz, 19940616 Presentation Support for Distributed Multimedia Applications John Bates University of Cambridge Computer Laboratory To my parents: Jean and Derek. Preface This report is based on a Ph.D. dissertation submitted by this author in January 1994. The work documented in this report also features in the
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR351-skb-Realtime-Mobile-Traffic.ps.gz, 19940920 Handling Realtime Traffic in Mobile Networks Subir Kumar Biswas Darwin College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy August 1994
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR308-jf10008-co-induction.ps.gz, 19941103 A Case Study of Co-induction in Isabelle HOL Jacob Frost y Computer Laboratory University of Cambridge e-mail:Jacob.Frost@cl.cam.ac.uk August 1993
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR347-ksj-reflections-on-trec.ps.gz, 19941129 Reflections on TREC Karen Sparck Jones Computer Laboratory, University of Cambridge New Museums Site, Pembroke Street Cambridge CB2 3QG, England sparckjones@cl.cam.ak.uk July 1994
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR334-lcp-final.coalgebra.ps.gz, 19950127 A Concrete Final Coalgebra Theorem for ZF Set Theory Lawrence C. Paulson lcp@cl.cam.ac.uk Computer Laboratory, University of Cambridge, England
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR359-jf10008-co-induction-in-isabelle.ps.gz, 19950220 A Case Study of Co-induction in Isabelle 1 Jacob Frost Computer Laboratory University of Cambridge e-mail:Jacob.Frost@cl.cam.ac.uk February 1995 1Supported by ESPRIT Basic Research Project 6453, Types for Proofs and Programs and the Danish Natural Science Research Council
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR361-rjb17-explicit-network-scheduling.ps.gz, 19950324 Explicit Network Scheduling Richard John Black Churchill College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy December 1994
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR312-lcp-set-II.ps.gz, 19950426 Set Theory for Verification: II Induction and Recursion Lawrence C. Paulson Computer Laboratory, University of Cambridge April 26, 1995
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz, 19950501 The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment Ole Rasmussen Computer Laboratory University of Cambridge March 1995
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR307-ksj-nl-processing-for-ir.ps.gz, 19950505 Natural language processing for information retrieval David D. Lewis AT&T Bell Laboratories Karen Sparck Jones Computer Laboratory, University of Cambridge July 1993
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR363-idbs1-names-higher-order-functions.ps.gz, 19950512 Names and Higher-Order Functions Ian David Bede Stark Queens' College A dissertation submitted to the University of Cambridge towards the degree of Doctor of Philosophy December 1994 University of Cambridge Computer Laboratory Technical Report No. 363 April 1995
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR367-ap-categorical-logic.ps.gz, 19950605 Categorical Logic A chapter in the forthcoming Volume VI of Handbook of Logic in Computer Science S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds), Oxford University Press Andrew M. Pitts Cambridge University Computer Laboratory Cambridge CB2 3QG, UK hap@cl.cam.ac.uki 18 May 1995 Categorical Logic
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR314-jac-practical-unif-parsing.ps.gz, 19950612 Practical Unification-based Parsing of Natural Language John Andrew Carroll Computer Laboratory University of Cambridge September 1993 PhD Thesis Acknowledgements1 I would like to thank Ted Briscoe, my supervisor, who prompted me to write this thesis. The ideas and suggestions he has come up with have
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR368-bs201-cogpit.ps.gz, 19950706 CogPiT \| Configuration of Protocols in TIP Burkhard Stiller University of Cambridge, Computer Laboratory New Museums Site, Pembroke Street Cambridge, CB2 3QR, England, U.K. Phone: +44 +1223 334476, FAX: +44 +1223 334678 E-Mail: Burkhard.Stiller@cl.cam.ac.uk
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR374-bs201-qos_updates.ps.gz, 19950706 A Framework for QoS Updates in a Networking Environment Burkhard Stiller University of Cambridge, Computer Laboratory New Museums Site, Pembroke Street Cambridge, CB2 3QR, England, U.K. Phone: +44 +1223 334476, FAX: +44 +1223 334678 E-Mail: Burkhard.Stiller@cl.cam.ac.uk
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR376-tr-multi-service-os.ps.gz, 19950710 The Structure of a Multi-Service Operating System Timothy Roscoe Queens' College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy April 1995 Summary Increases in processor speed and network bandwidth have led to workstations being used to process multimedia data in
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR380-bs201-qos_issues.ps.gz, 19950912 Quality-of-Service Issues in Networking Environments Burkhard Stiller University of Cambridge, Computer Laboratory New Museums Site, Pembroke Street Cambridge, CB2 3QR, England, U.K. Phone: +44 +1223 334476, FAX: +44 +1223 334678 E-Mail: Burkhard.Stiller@cl.cam.ac.uk
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR199-rjb-mjcg-jmjh-jvt-HOL-verification-ELLA.ps.gz, 19950920 The HOL Verification of ELLA Designs1 Richard Boulton, Mike Gordon, John Herbert, John Van Tassel University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG United Kingdom
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR304-lcp-coinduction.ps.gz, 19960209 Mechanizing Coinduction and Corecursion in Higher-order Logic Lawrence C. Paulson Computer Laboratory, University of Cambridge
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR390-rjb-Syn-single-language.ps.gz, 19960318 Syn: A Single Language for Specifying
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR393-sac-performance-management-in-ATM-networks.ps.gz, 19960421 Performance Management in ATM Networks Simon Andrew Crosby St. John's College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy May 1995
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR394-lcp-mutilated-chess-board.ps.gz, 19960514 A Simple Formalization and Proof for the Mutilated Chess Board Lawrence C. Paulson Computer Laboratory, University of Cambridge
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR356-ksj-approaches-to-text-retrieval.ps.gz, 19960603 Simple, proven approaches to text retrieval S.E. Robertson and K. Sparck Jones Department of Information Science, City University ser@is.city.ac.uk Computer Laboratory, University of Cambridge ksj@cl.cam.ac.uk May, 1996 Technical Report 356, Computer Laboratory, 1994 version with updates
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR397-br212-optimal-routing-in-2-jump-circulant-networks.ps.gz, 19960603 Optimal Routing in 2-jump Circulant Networks Borut Robi<=c University of Cambridge Computer Laboratory Systems Research Group New Museums Site, Pembroke Street, Cambridge CB2 3QG, UK May 1996
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR362-mh10006-w-learning.ps.gz, 19960613 W-learning: Competition among selfish Q-learners Mark Humphrys University of Cambridge, Computer Laboratory http://www.cl.cam.ac.uk/users/mh10006 y April 1995
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR403-prb12-devices-in-a-multi-service-os.ps.gz, 19960628 Devices in a Multi-Service Operating System Paul Ronald Barham Churchill College University of Cambridge A dissertation submitted for the degree of Doctor of Philosophy July 1996 Summary Increases in processor speed and network and device bandwidth have led to general purpose workstations being called
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz, 19960926 Generic Automatic Proof Tools1 Lawrence C. Paulson Computer Laboratory, University of Cambridge May 1996 1This will be a chapter in the book Automated Reasoning and Its Applications, being edited by Robert Veroff and to be published by The MIT Press in 1997. Additional information may be obtained from
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR407-ss249-L4-Microkernel.ps.gz, 19960927 The L4 Microkernel on Alpha Design and Implementation Sebastian Sch onberg September 27, 1996 ii Preface 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
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR377-lcp-mechanising-set-theory.ps.gz, 19961002 Mechanizing Set Theory Cardinal Arithmetic and the Axiom of Choice Lawrence C. Paulson Computer Laboratory, University of Cambridge email: lcp@cl.cam.ac.uk Krzysztof Grabczewski Nicholas Copernicus University, Toru n, Poland email: kgrabcze@mat.uni.torun.pl (Received ..... ; Accepted in final form
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR384-scc1000-Securing-ATM-Networks.ps.gz, 19961024 UNIVERSITY OF CAMBRIDGE COMPUTER LABORATORY Technical Report No. 384 SECURING ATM NETWORKS by Shaw-Cheng Chuang July 1995 University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG England Telephone Cambridge (01223) 334600 Securing ATM Networks Shaw-Cheng Chuang
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR406-lcp-Tool-Support-for-Logics-of-Programs.ps.gz, 19961125 Tool Support for Logics of Programs Lawrence C. Paulson Computer Laboratory, University of Cambridge November 1996 Key words: proof tools / generic reasoning / logic programming / logical variables / uniocation / Isabelle / higher-order logic / set theory / inductive deonitions / cryptographic protocols
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR408-jrh-Theorem-Proving-with-the-Real-Numbers.ps.gz, 19961206 Theorem Proving with the Real Numbers John Robert Harrison Churchill College A dissertation submitted for the degree of Doctor of Philosophy in the University of Cambridge Preface This technical report is a slightly revised version of my University of Cambridge PhD thesis, incorporating a few changes
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR405-rjb-tool-formal-comp-lang.ps.gz, 19961211 A Tool to Support Formal Reasoning about Computer Languages Richard J. Boulton University of Cambridge Computer Laboratory New Museums Site, Pembroke Street Cambridge CB2 3QG, United Kingdom November 1996
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR410-jrh-proof-style.ps.gz, 19970106 Proof Style John Harrison University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG England jrh@cl.cam.ac.uk http://www.cl.cam.ac.uk/users/jrh January 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR413-lcp-Mechanized-Proofs-of-Security-Protocols-Needham-Schroeder-with-Public-Keys.ps.gz, 19970130 Mechanized Proofs of Security Protocols: Needham-Schroeder with Public Keys Lawrence C. Paulson Computer Laboratory University of Cambridge lcp@cl.cam.ac.uk January 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR409-lcp-Proving-Properties-of-Security-Protocols-by-Induction.ps.gz, 19970130 Proving Properties of Security Protocols by Induction Lawrence C. Paulson Computer Laboratory University of Cambridge December 1996
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR421-mn200-c-semantics.ps.gz, 19970513 An abstract dynamic semantics for C Michael Norrish Computer Laboratory, University of Cambridge May 6, 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR426-mh10006-phd.ps.gz, 19970605 Action Selection methods using Reinforcement Learning Mark Humphrys Trinity Hall A dissertation submitted for the degree of Doctor of Philosophy in the University of Cambridge Technical Report June 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR418-lcp-recur.ps.gz, 19970617 Mechanized Proofs for a Recursive Authentication Protocol1 Lawrence C. Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England lcp@cl.cam.ac.uk 1An abridged version of this paper appeared in the Proceedings of the 10th Computer Security Foundations Workshop, 10{12
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR428-jrh-tang.ps.gz, 19970626 Floating point verification in HOL Light: the exponential function John Harrison University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG England jrh@cl.cam.ac.uk http://www.cl.cam.ac.uk/users/jrh June 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR429-adg-pdh-sbl-objects.ps.gz, 19970711 Compilation and Equivalence of Imperative Objects Andrew D. Gordon University of Cambridge Computer Laboratory adg@cl.cam.ac.uk Paul D. Hankin University of Cambridge Computer Laboratory pdh13@cam.ac.uk S. B. Lassen BRICS Department of Computer Science University of Aarhus thales@brics.dk July 11, 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR432-lcp-Yahalom.ps.gz, 19970724 On Two Formal Analyses of the Yahalom Protocol Lawrence C. Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England lcp@cl.cam.ac.uk July 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR440-lcp-inductive-analysis-of-TLS.ps.gz, 19971216 Inductive Analysis of the Internet Protocol TLS Lawrence C. Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England lcp@cl.cam.ac.uk 16 December 1997
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR441-lcp-Generic-Tableau-Prover.ps.gz, 19980109 A Generic Tableau Prover and its Integration with Isabelle Lawrence C. Paulson lcp@cl.cam.ac.uk 9 January 1998
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR442-jdf21-lcp-Nonstandard-Analysis-and-Geometry-Theorem-Proving.ps.gz, 19980113 A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia Jacques D. Fleuriot Lawrence C. Paulson Computer Laboratory { University of Cambridge New Museums Site, Pembroke Street Cambridge CB2 3QG fjdf21,lcpg@cl.cam.ac.uk January 1998
	ftp://ftp.cl.cam.ac.uk/papers/reports/TR443-lcp-Inductive-Approach-to-Verifying-Cryptographic-Protocols.ps.gz, 19980206 The Inductive Approach to Verifying Cryptographic Protocols Lawrence C. Paulson Computer Laboratory University of Cambridge Pembroke Street Cambridge CB2 3QG England lcp@cl.cam.ac.uk 6 February 1998