# TECHNICAL REPORT DATABASE # # Original design: Markus Kuhn -- 2002-01 # # Maintenance history: # # mgk25 (2002-01 - 2009-10) # ncc25 (2009-10 - now) # # The format of this database is as follows: # # - The character encoding is UTF-8 (Unicode/ISO 10646, Normalization # Form C). Characters that are not available in TeX should be avoided # (including ' and "). Do not use any TeX sequences such as “--”. # Instead use UTF-8 characters such as # # Single quotes: ‘’ double quotes: “” en/em dash: –— # Greek letters: ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣ ΤΥΦΧΨΩ # αβγδεζηθικλμνξοπρςστυφχψω # # - Each technical report is represented by a *single* line of the form # # number|date|title|authors|pages|notes # # as in # # 987|2002-01|A tech-report system|Markus G. Kuhn |5|front=Demo # # - The number of pages given in the pages field is the total number # of pages in all parts. Leave the field empty if the number of # pages is not known. For older, paper-only reports, it is # sufficient to give the number of the last printed page. If there # are several paginations, add their respective last page numbers # up, to get a good estimate of the total number of printed pages. # (For newer reports, the last printed page number and the total # number of pages in the PDF file should be identical, see ISO 5966.) # # - The date is given in one of the all-numeric (ISO 8601) forms # # YYYY # YYYY-MM <- preferred # YYYY-MM-DD # # - In a title, a \\ can be used to separate a title and subtitles. This # will force a line break on the formatted title page. It will appear as # inserted as “ : ” in bibliographic entries (unless # it follows immediately a punctuation character). All other # characters and character sequences have their normal # UTF-8 meaning. In particular, do *not* use TeX codes. # # The capitalization of titles should be like in normal sentences, # just like the University Library catalog does it. # # - The names of several authors are to be separated by “, ” (comma # followed by space). The last word in a single author’s name # will be interpreted as the surname. Spaces inside surnames # must therefore be encoded as no-break spaces (U+00A0). # # - The name of each author can optionally be followed by “ ” # for unique identification of authors and automatic creation of links # to their departmental home page. # # - If the title starts with 'Proceedings ', the people listed in the # authors field will be considered editors. # # - The notes field serves to provide additional attributes for # a report. Many of these place additional remarks onto the # front or back of the title page. Standard remarks are defined for # common types of documents, e.g. PhD thesis. Several of the following # notes can be specified, separated by “|”, but each type of note can # only appear once for a report: # # front=... Prints a large note into the lower left corner # of the title page # # back=... Prints a small note on the verso of the title # page, below the copyright notice; you can # use \\ to start a new line and \_ to start # a new paragraph # # The following notes not only place a note on the back side # of the title page, but also may mark the report in various indices # as being based on a dissertation: # # phd # phd=college,date # This has the same effect as # # back=This technical report is based on a # dissertation submitted by the author for # the degree of Doctor of Philosophy to the # University of Cambridge, . # # ophd=institution,date # Same for PhDs submitted to other Universities # than Cambridge. # # mphil-cstit=college,date # This is the same as # # back=This technical report is based on a # dissertation submitted by the author for # the degree of Master of Philosophy # (Computer Speech, Text and Internet Technology) # to the University of Cambridge, . # # mphil-acs=college,date # This includes the same effect as # # back=This technical report is based on a # dissertation submitted by the author for # the degree of Master of Philosophy # (Advanced Computer Science) to the # University of Cambridge, . # # cst-part2=college,date # This is the same as # # back=This technical report is based on a # dissertation submitted by the author # for the degree of Bachelor of Arts # (Computer Science Tripos) to the # University of Cambridge, . # # cst-part3=college,date # This is the same as # # back=This technical report is based on a # dissertation submitted by the author # for the degree of Master of Engineering # (Computer Science Tripos) to the # University of Cambridge, . # # Some other notes or attributes that can be set: # # colour Adds a note saying that some figures in this # report will only make sense if printed in colour. # # contrib=contribution::contributor, contributor, ...;;... # The type of contribution should be phrased such that # it can be printed followed by "by" and the list # of the contributor's names (which follows the same # syntax as the authors names). Examples: # contrib=translation::John Smith;; # illustrations::J. Doe, J. Dummy;; # new preface::E. Xample, A. Uthor # # to-appear=date # The final version of the report has not yet # been submitted, but the author was given a # report number in advance. # # updated=date{,date} # The present report incorporates minor changes # that were made after it was first released. These # modifications were released at the comma-separated # listed dates. This list does not include the # original publication date of the report, which # remains unaffected. The dates are sorted oldest # update first. # # deleted{=date,reason} # The report has been removed from the repository. # Rather than just deleting the record and leaving # a number gap, use this attribute to suppress # a report while preserving its historic metadata. # # copyright-owner=name(s) # By default, the verso of the title page # contains a copyright message that lists all # the authors of a report. This attribute # replaces those names listed in the copyright # note. Provide the list of names in the same # form as in the authors field, i.e. separated # by “, ”. # # add-copyright-owner=name(s) # This attribute adds one or more additional # names to the copyright note, e.g. a sponsoring # organization that requires this. Provide the # list of names in the same form as in the # authors field, i.e. separated by “, ”. # # copyright-year=year # By default, the copyright year is taken from # the publication date, however for historic # documents an earlier year may be more # appropriate. # # cc=by Indicate that the authors have licensed their # technical report under the terms of the # Creative Commons “Attribution 4.0 # International (CC BY 4.0)” licence. # # cc=by-nd Indicate that the authors have licensed their # technical report under the terms of the # Creative Commons “Attribution-NoDerivatives 4.0 # International (CC BY-ND 4.0)” licence. # # isbn=978-0-901224-xy-z # On request, we can assign an ISBN to a # technical report, e.g. if this is a # requirement of a funding body. We currently # allocate from a block of 100 ISBNs that the # department acquired in the 1970s. The range # xy=00-03 appears to have been allocated in the # early 1970s. We started allocating selected # technical reports from xy=10 upwards, to leave # a safety gap to the few known 1970s # allocations, just in case there were more that # we haven't discovered yet. The ISBN must be # entered here as 13 digits separated by four # hyphens, as per BS ISO 2108:2017. The final # digit (z) must be calculated as a weighted sum # of the preceding digits modulus 10. # # - Header comments have “#” in the first column # # - Title page details are specified in the form “parameter=...” # for the entire series. Each parameter is specified on a single # line that appears before the first technical report entry. # Parameter names have the regular expression form “[a-z]+”. # # This database is the official record of which report number has been # assigned to which report. It is also used as a data source to print # title pages as well as content lists (paper and web). # # As the software is designed to be usable by other departments, # this database file contains all information that is specific to a # particular report series: # # SERIES PARAMETERS # # The name of the department issuing this report series: # department=Computer Laboratory # # The following uppercase abbreviation should uniquely identify the # department within the University of Cambridge in a uniform technical # report number scheme. Preferably use code from XXX.cam.ac.uk CUDN # domain name, e.g. CL for the Computer Laboratory (cl.cam.ac.uk). # [Note from mgk25: I investigated registering an International Standard # Report Number (ISRN) according to ISO 10444 and ANSI/NISO Z39.23, # but I was told that this scheme is not operating at the moment, # so we will use an ad-hoc code. # http://www.fiz-karlsruhe.de/fiz/service/isrn.html] # code=UCAM-CL-TR # # If your department’s technical report series has been assigned an # International Standard Serial Number, then insert it here (eight digits # with a hyphen in the centre). If not, then best apply for one at # http://www.bl.uk/services/bsds/nbs/issn.html. It costs nothing and # is easily done. # Computer Laboratory Technical Report = ISSN 1476-2986 # issn=1476-2986 # # If you are assigning a Digital Object Identifier (DOI) to each # technical report, then set here the DOI prefix allocated to you for # this purpose. The per-report DOI will then be generated by appending # to that prefix “/tr-”, where is the report’s number. # doiprefix=10.48456 # # Provide the full address of your department including a telephone # contact number. Use \\ at the end of each line. # address=15 JJ Thomson Avenue\\Cambridge CB3 0FD\\United Kingdom\\phone +44 1223 763500 # # URL of the department # depturl=https://www.cl.cam.ac.uk/ # # URL where the technical reports from your department # can be downloaded over the Internet. # reporturl=https://www.cl.cam.ac.uk/techreports/ # # Editor of the technical report series # #editor=Markus Kuhn # # # TECHNICAL REPORT ENTRIES # 1|1974-10|The JACKDAW database package|M.F. Challis|15| 2|1974-10|Scheduling for a share of the machine|J. Larmouth|29| 3|1975-04|A replacement for the OS/360 disc space management routines|A.J.M. Stoneley|7| 4|1975-04|The dynamic creation of I/O paths under OS/360-MVT|A.J.M. Stoneley|16| 5|1976-04|Parrot – A replacement for TCAM|P. Hazel , A.J.M. Stoneley|25| 6|1977-12|System programming in a high level language|Andrew D. Birrell|125|phd=Trinity College,1977-12 7|1978-04|Local area computer communication networks|Andrew Hopper |192|phd=Trinity Hall,1978-04 # Report 8 apparently does not exist 9||Evaluation of a protection system|Douglas John Cook|181|phd=Gonville & Caius College,1978-04 10||Prediction oriented description of database systems|Mark Theodore Pezarro|190|phd=Darwin College,1978-10 11||Automatic resolution of linguistic ambiguities|Branimir Konstatinov Boguraev |222|phd=Trinity College,1979-08 12|1979-09|HASP “IBM 1130” multileaving remote job entry protocol with extensions as used on the University of Cambridge IBM 370/165|M.R.A. Oakley, P. Hazel |28| 13|1980|Resource allocation and job scheduling|Philip Hazel |41| 14|1980-06|Store to store swapping for TSO under OS/MVT|J.S. Powers|28| 15||The implementation of BCPL on a Z80 based microcomputer|I.D. Wilson |68|cst-part2=Downing College,1980-05 16|1981-02|Reliable storage in a local network|Jeremy Dion|142|phd=Darwin College,1981-02 17|1982|Three papers on parsing|B.K. Boguraev , K. Spärck Jones , J.I. Tait |22| 18|1981-11|Automatic mesh generation of 2 & 3 dimensional curvilinear manifolds|Burkard Wördenweber|128|phd=St John’s College,1981-11 19|1981-09|Analysis and inference for English|Arthur William Sebright Cater|223|phd=Queens’ College,1981-09 20|1982-02|On using Edinburgh LCF to prove the correctness of a parsing algorithm|Avra Cohn, Robin Milner |23| 21|1982-04|The correctness of a precedence parsing algorithm in LCF|A. Cohn|38| 22||Constraints in CODD|M. Robson|18| 23||Two papers about the scrabble summarising system|J.I. Tait |12| 24|1982-03|Steps towards natural language to data language translation using general semantic information|B.K. Boguraev , K. Spärck Jones |8| 25|1982-05|A clustering technique for semantic network processing|Hiyan Alshawi|9| 26||Portable system software for personal computers on a network|Brian James Knight|204|phd=Churchill College,1982-04 27|1981-09|Exception handling in domain based systems|Martyn Alan Johnson |129|phd=Churchill College,1981-09 28|1982-08|Poly report|D.C.J. Matthews|17| 29|1982-05|Introduction to Poly|D.C.J. Matthews|24| 30|1982-10|A portable BCPL library|John Wilkes|31| 31|1982-11|Ponder and its type system|J. Fairbairn |42| 32|1982-11|How to drive a database front end using general semantic information|B.K. Boguraev , K. Spärck Jones |20| 33|1982-10|An island parsing interpreter for Augmented Transition Networks|John A. Carroll |50| 34|1983-01|Recent developments in LCF: examples of structural induction|Larry Paulson |15| 35|1983-02|Rewriting in Cambridge LCF|Larry Paulson |32| 36|1983-03|The revised logic PPLAMBDA\\A reference manual|Lawrence Paulson |28| 37||Representation and authentication on computer networks|Christopher Gray Girling|154|phd=Queens’ College,1983-04 38|1982-11|Views and imprecise information in databases|Mike Gray|119|phd=,1982-11 39|1983-07|Tactics and tacticals in Cambridge LCF|Lawrence Paulson |26| 40|1983-10|The SKIM microprogrammer’s guide|W. Stoye|33| 41|1983-09|LCF_LSM, A system for specifying and verifying hardware|Mike Gordon |53| 42|1983-09|Proving a computer correct with the LCF_LSM hardware verification system|Mike Gordon |49| 43|1983-02|Extending the local area network|Ian Malcom Leslie |71|phd=Darwin College,1983-02 44|1983-11|Structural induction in LCF|Lawrence Paulson |35| 45|1983-07|Compound noun interpretation problems|Karen Spärck Jones |16| 46|1985-05|Intelligent network interfaces|Nicholas Henry Garnett|140|phd=Trinity College,1983-05 47||Automatic summarising of English texts|John Irving Tait |137|phd=Wolfson College,1982-12 48|1983-11|A mechanism for the accumulation and application of context in text processing|Hiyan Alshawi|17| 49||Programming language design with polymorphism|David Charles James Matthews|143|phd=Wolfson College,1983 50|1984-03|Verifying the unification algorithm in LCF|Lawrence Paulson |28| 51|1984-07|Using information systems to solve recursive domain equations effectively|Glynn Winskel , Kim Guldstrand Larsen|41| 52||The design of a ring communication network|Steven Temple|132|phd=Corpus Christi College,1984-01 53|1984-07|A new type-checker for a functional language|Jon Fairbairn |16| 54|1984-08|Lessons learned from LCF|Lawrence Paulson |16| 55|1984-08|Executing temporal logic programs|Ben Moszkowski|27| 56|1984-09|A new scheme for writing functional operating systems|William Stoye|30| 57|1984-10|Constructing recursion operators in intuitionistic type theory|Lawrence C. Paulson |46| 58|1984-10|Categories of models for concurrency|Glynn Winskel |35| 59|1984-11|On the composition and decomposition of assertions|Glynn Winskel |35| 60||Memory and context mechanisms for automatic text processing|Hiyan Alshawi|192|phd=Trinity Hall,1983-12 61|1984-12|User models and expert systems|Karen Spärck Jones |44| 62||Constraint enforcement in a relational database management system|Michael Robson|106|phd=St John’s College,1984-03 63|1985-02|Poly manual|David C.J. Matthews|46| 64|1985-02|A framework for inference in natural language front ends to databases|Branimir K. Boguraev , Karen Spärck Jones |73| 65|1985-05|Introduction to the programming language “Ponder”|Mark Tillotson |57| 66|1985-05|A formal hardware verification methodology and its application to a network interface chip|M.J.C. Gordon , J. Herbert|39| 67|1985-05|Natural deduction theorem proving via higher-order resolution|Lawrence C. Paulson |22| 68|1985-07|HOL\\A machine oriented formulation of higher order logic|Mike Gordon |52| 69|1985-06|Proving termination of normalization functions for conditional expressions|Lawrence C. Paulson |16| 70|1984-12|A remote procedure call system|Kenneth Graham Hamilton|109|phd=Wolfson College,1984-12 71|1985-08|Executing temporal logic programs|Ben Moszkowski|96| 72|1985-05|Logic programming and the specification of circuits|W.F. Clocksin |13| 73||Resource management in a distributed computing system|Daniel Hammond Craft|116|phd=St John’s College,1985-03 74|1985-08|Hardware verification by formal proof|Mike Gordon |6| 75|1985-05|Design and implementation of a simple typed language based on the lambda-calculus|Jon Fairbairn |107|phd=Gonville & Caius College,1984-12 76|1985-08|Preserving abstraction in concurrent programming|R.C.B. Cooper, K.G. Hamilton|16| 77|1985-09|Why higher-order logic is a good formalisation for specifying and verifying hardware|Mike Gordon |28| 78|1985-09|A complete proof system for SCCS with model assertions|Glynn Winskel |23| 79||Petri nets, algebras and morphisms|Glynn Winskel |38| 80|1985-11|Interactive theorem proving with Cambridge LCF\\A user’s manual|Lawrence C. Paulson |140| 81|1985-12|The implementation of functional languages using custom hardware|William Robert Stoye|151|phd=Magdalene College,1985-05 82|1985-12|Natural deduction proof as higher-order resolution|Lawrence C. Paulson |25| 83||Operating system design for large personal workstations|Ian David Wilson |203|phd=Darwin College,1985-07 84|1986-04|BSPL:\\a language for describing the behaviour of synchronous hardware|Martin Richards |56| 85|1986-04|Category theory and models for parallel computation|Glynn Winskel |16| 86|1986-04|The Entity System: an object based filing system|Stephen Christopher Crawley|120|phd=St John’s College,1985-12 87|1986-05|Computer-aided type face design|Kathleen Anne Carter|172|phd=King’s College,1985-11 88|1986-05|A shallow processing approach to anaphor resolution|David Maclean Carter|233|phd=King’s College,1985-12 89|1986-06|Making form follow function\\An exercise in functional programming style|Jon Fairbairn |9| 90|1986-06|The Cambridge Fast Ring networking system (CFR)|Andy Hopper , Roger M. Needham |25| 91|1986-09|Hardware verification using higher-order logic|Albert Camilleri , Mike Gordon , Tom Melham |25| 92|1986-06|Implementation and programming techniques for functional languages|Stuart Charles Wray|117|phd=Christ’s College,1986-01 93|1986-06|Automated design of an instruction set for BCPL|J.P. Bennett|56| 94|1986-06|A mechanized proof of correctness of a simple counter|Avra Cohn, Mike Gordon |80| 95|1986-07|Event structures\\Lecture notes for the Advanced Course on Petri Nets|Glynn Winskel |69| 96|1986-10|Models and logic of MOS circuits\\Lectures for the Marktoberdorf Summerschool, August 1986|Glynn Winskel |47| 97|1986-10|A study on abstract interpretation and “validating microcode algebraically”|Alan Mycroft |22| 98|1986-10|Power-domains, modalities and the Vietoris monad|E. Robinson|16| 99|1986-08|An overview of the Poly programming language|David C.J. Matthews|11| 100|1986-12|Proving a computer correct in higher order logic|Jeff Joyce , Graham Birtwistle, Mike Gordon |57| 101|1986-12|Binary routing networks|David Russel Milway|131|phd=Darwin College,1986-12 102|1987-01|A persistent storage system for Poly and ML|David C.J. Matthews|16| 103|1987-01|HOL\\A proof generating system for higher-order logic|Mike Gordon |56| 104|1987-01|A proof of correctness of the Viper microprocessor: the first level|Avra Cohn|46| 105|1987-04|A compositional model of MOS circuits|Glynn Winskel |25| 106|1987-05|Abstraction mechanisms for hardware verification|Thomas F. Melham |26| 107|1987-05|DI-domains as a model of polymorphism|Thierry Coquand, Carl Gunter, Glynn Winskel |19| 108|1987-06|Workstation design for distributed computing|Andrew John Wilkes|179|phd=Wolfson College,1984-06 109|1987-07|Hardware verification of VLSI regular structures|Jeffrey Joyce |20| 110|1987-07|Relating two models of hardware|Glynn Winskel |16| 111|1987-06|Realism about user modelling|K. Spärck Jones |32| 112|1987-08|Reducing thrashing by adaptive backtracking|D.A. Wolfram |15| 113|1987-08|The representation of logics in higher-order logic|Lawrence C. Paulson |29| 114|1987-09|An architecture for integrated services on the local area network|Stephen Ades|166|phd=Trinity College,1987-01 115|1987-08|Formal validation of an integrated circuit design style|I.S. Dhingra|29| 116|1987-09|Domain theoretic models of polymorphism|Thierry Coquand, Carl Gunter, Glynn Winskel |52| 117|1987-10|Distributed computing with RPC: the Cambridge approach|J.M. Bacon , K.G. Hamilton|15| 118|1987-05|Material concerning a study of cases|B.K. Boguraev , K. Spärck Jones |31|back=This study is reported in B.K. Boguraev and K. Spärck Jones, ‘A note on a study of cases’, Computaational Linguistics 13, 1987. The attached material consists first of an extended account of the study with its own illustrative examples, and second of the full data analysis, printed in two different sort orders. 119|1987-07|Pilgrim: a debugger for distributed systems|Robert Cooper|19| 120|1987-11|Block encryption|D. Wheeler |4| 121|1987-12|A high-level petri net specification of the Cambridge Fast Ring M-access service|Jonathan Billington|31| 122|1988-02|Temporal abstraction of digital designs|John Herbert|34| 123|1988-02|Case study of the Cambridge Fast Ring ECL chip using HOL|John Herbert|38| 124|1988-02|Formal verification of basic memory devices|John Herbert|46| 125|1988-02|An operational semantics for Occam|Juanito Camilleri |24| 126|1988-02|Reasoning about the function and timing of integrated circuits with Prolog and temporal logic|M.E. Leeser |50| 127|1988-02|A development environment for large natural language grammars|John Carroll , Bran Boguraev , Claire Grover, Ted Briscoe |44| 128|1988-02|Debugging concurrent and distributed programs|Robert Charles Beaumont Cooper|111|phd=Churchill College,1987-12 129|1988-03|A methodology for automated design of computer instruction sets|Jeremy Peter Bennett|147|phd=Emmanuel College,1987-01 130|1988-03|The foundation of a generic theorem prover|Lawrence C Paulson |44|front=This paper is a revised version of UCAM-CL-TR-113. 131|1986-12|Architecture problems in the construction of expert systems for document retrieval|Karen Spärck Jones |28| 132|1988-04|Reasoning about the function and timing of integrated circuits with Prolog and temporal logic|Miriam Ellen Leeser |151|phd=Queens’ College,1987-12 133|1988-05|A preliminary users manual for Isabelle|Lawrence C. Paulson |81| 134|1988-05|Correctness properties of the Viper black model: the second level|Avra Cohn|114| 135|1988-05|Using recursive types to reason about hardware in higher order logic|Thomas F. Melham |30| 136|1988-06|Formal specification and verification of asynchronous processes in higher-order logic|Jeffrey J. Joyce |45| 137|1988-06|Mass terms and plurals: from linguistic theory to natural language processing|F.V. Hasle|171| 138|1988-06|Authentication: a practical study in belief and action|Michael Burrows , Martín Abadi, Roger Needham |19| 139|1988-06|Petri net theory: a survey|Paul R. Manson|77| 140|1988-07|Executing behavioural definitions in higher order logic|Albert John Camilleri |183|phd=Darwin College,1988-02 141|1988-07|Reliable management of voice in a distributed system|Roy Want|127|phd=Churchill College,1987-12 142|1988-07|A fast packet switch for the integrated services backbone network|Peter Newman |24| 143|1988-08|Experience with Isabelle\\A generic theorem prover|Lawrence C. Paulson |20| 144|1988-08|An operational semantics for occam|Juanito Camilleri |27|front=This is an extended version of UCAM-CL-TR-125, in which we include the operational semantics of priority alternation. 145|1988-09|Mechanizing programming logics in higher order logic|Michael J.C. Gordon |55| 146|1988-09|Automating recursive type definitions in higher order logic|Thomas F. Melham |64| 147|1988-09|Formal specification and verification of microprocessor systems|Jeffrey Joyce |24| 148|1988-09|Extending coloured petri nets|Jonathan Billington|82| 149|1988-10|Improving security and performance for capability systems|Paul Ashley Karger |273|phd=Wolfson College,1988-03 150|1988-10|Simulation as an aid to verification using the HOL theorem prover|Albert John Camilleri |23| 151|1988-11|Formalising an integrated circuit design style in higher order logic|Inderpreet-Singh Dhingra|195|phd=King’s College,1988-03 152|1988-11|Motion development for computer animation|Andrew Mark Pullen|163|phd=Churchill College,1987-08 153|1988-12|Efficient data sharing|Michael Burrows |99|phd=Churchill College,1988-09 154|1989-01|A natural language interface to an intelligent planning system|I.B. Crabtree, R.S. Crouch , D.C. Moffat, N.J. Pirie, S.G. Pulman , G.D. Ritchie, B.A. Tate|14|back=This project is supported by the Alvey Directorate and the Science and Engineering Research Council (Alvey IKBS 179, SERC GR/D/83507). This paper is to appear in the Proceedings of the 1988 UK IT Conference, Swansea. 155|1989-01|Computational morphology of English|S.G. Pulman , G.J. Russell, G.D. Ritchie, A.W. Black|15| 156|1989-01|Events and VP modifiers|Steve Pulman |10| 157|1989-01|Introducing a priority operator to CCS|Juanito Camilleri |19| 158|1988-08|Tailoring output to the user:\\What does user modelling in generation mean?|Karen Spärck Jones |21| 159|1989-01|Non-trivial power types can’t be subtypes of polymorphic types|Andrew M. Pitts |12| 160|1989-02|PFL+: A Kernal Scheme for Functions I/O|Andrew Gordon|26| 161|1989-02|Papers on Poly/ML|D.C.J. Matthews|150| 162|1989-04|The Alvey natural language tools grammar (2nd Release)|Claire Grover, Ted Briscoe , John Carroll , Bran Boguraev |90| 163|1989-02|Inference in a natural language front end for databases|Ann Copestake , Karen Spärck Jones |87| 164|1988-10|A matrix key distribution system|Li Gong , David J. Wheeler |20| 165|1989-03|Fast packet switching for integrated services|Peter Newman |145|phd=Wolfson College,1988-12 166|1989-03|Evolution of operating system structures|Jean Bacon |28| 167|1989-03|A verified compiler for a verified microprocessor|Jeffrey J. Joyce |67| 168|1989-04|Distributed computing with a processor bank|J.M. Bacon , I.M. Leslie , R.M. Needham |15| 169|1989-04|Filing in a heterogeneous network|Andrew Franklin Seaborne |131|phd=Churchill College,1987-07 170|1989-05|Ordered rewriting and confluence|Ursula Martin , Tobias Nipkow |18| 171|1989-06|Some types with inclusion properties in ∀, →, μ|Jon Fairbairn |10| 172|1989-07|A theoretical framework for computer models of cooperative dialogue, acknowledging multi-agent conflict|Julia Rose Galliers|226| 173|1989-07|Programming in temporal logic|Roger William Stephen Hale|182|phd=Trinity College,1988-10 174|1989-08|General theory relating to the implementation of concurrent symbolic computation|James Thomas Woodchurch Clarke|113|phd=Trinity College,1989-01 175|1989-08|A formulation of the simple theory of types (for Isabelle)|Lawrence C. Paulson |32| 176|1989-08|Implementing aggregates in parallel functional languages|T.J.W. Clarke |13| 177|1989-09|Experimenting with Isabelle in ZF Set Theory|P.A.J. Noel|40| 178|1989-09|Totally verified systems:\\linking verified software to verified hardware|Jeffrey J. Joyce |25| 179|1989-09|Automating Squiggol|Ursula Martin , Tobias Nipkow |16| 180|1989-09|Formal verification of data type refinement:\\Theory and practice|Tobias Nipkow |31| 181|1989-09|Proof transformations for equational theories|Tobias Nipkow |17| 182|1989-10|The theory and implementation of a bidirectional question answering system|John M. Levine , Lee Fedder |27| 183|1989-10|The specification and verification of sliding window protocols in higher order logic|Rachel Cardell-Oliver |25| 184|1989-10|Site interconnection and the exchange architecture|David Lawrence Tennenhouse |225|phd=Darwin College,1988-09 185|1989-12|Logics of domains|Guo Qiang Zhang |250|phd=Trinity College,1989-05 186|1990-01|Protocol design for high speed networks|Derek Robert McAuley |100|phd=Fitzwilliam College,1989-09 187|1989-09|Natural language interfaces to databases|Ann Copestake , Karen Spärck Jones |36| 188|1990-01|Specification of computer architectures:\\a survey and annotated bibliography|Timothy E. Leonard |42| 189|1990-01|Isabelle tutorial and user’s manual|Lawrence C. Paulson , Tobias Nipkow |142| 190|1990-01|Some notes on mass terms and plurals|Ann Copestake |65| 191|1990-02|An architecture for real-time multimedia communications systems|Cosmos Nicolaou |30| 192|1990-05|Designing a theorem prover|Lawrence C. Paulson |57| 193|1990-05|Belief revision and a theory of communication|Julia Rose Galliers|30| 194|1990-03|Proceedings of the First Belief Representation and Agent Architectures Workshop|Julia Rose Galliers|199| 195|1990-05|Multi-level verification of microprocessor-based systems|Jeffrey J. Joyce |163|phd=Pembroke College,1989-12 196|1990-06|The semantics of VHDL with Val and Hol:\\towards practical verification tools|John Peter Van Tassell |77| 197|1990-07|The semantics and implementation of aggregates\\or\\how to express concurrency without destroying determinism|Thomas Clarke|25| 198|1990-08|Evaluation Logic|Andrew M. Pitts |31| 199|1990-08|The HOL verification of ELLA designs|Richard Boulton , Mike Gordon , John Herbert, John Van Tassel |22| 200|1990-08|Type classes and overloading resolution via order-sorted unification|Tobias Nipkow , Gregor Snelting|16| 201|1990-08|Formalizing abstraction mechanisms for hardware verification in higher order logic|Thomas Frederick Melham |233|phd=Gonville & Caius College,1989-08 202|1990-08|Three-dimensional integrated circuit layout|Andrew Charles Harter |179|phd=Corpus Christi College,1990-04 203|1990-08|Subtyping in Ponder\\(preliminary report)|Valeria C.V. de Paiva |35| 204|1990-08|New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic|Roy L. Crole , Andrew M. Pitts |37| 205||Logic programming, functional programming and inductive definitions|Lawrence C. Paulson , Andrew W. Smith|29| 206|1990-08|Formal verification of real-time protocols using higher order logic|Rachel Cardell-Oliver |36| 207|1990-10|Video replay in computer animation|Stuart Philip Hawkins |161|phd=Queens’ College,1989-12 208|1990-10|Categorical combinators for the calculus of constructions|Eike Ritter |43| 209|1990-11|Efficient memory-based learning for robot control|Andrew William Moore |248|phd=Trinity Hall,1990-10 210||Higher-order unification, polymorphism, and subsorts|Tobias Nipkow |15| 211|1990-11|The role of artificial intelligence in information retrieval|Karen Spärck Jones |13| 212|1990-12|A distributed and-or parallel Prolog network|K.L. Wrench |82| 213|1991-01|The Dialectica categories|Valeria Correa Vaz de Paiva |82|phd=Lucy Cavendish College,1988-11 214|1991-02|Integrating knowledge of purpose and knowledge of structure for design evaluation|J.A. Bradshaw , R.M. Young|20| 215||A structured approach to the verification of low level microcode|Paul Curzon |265|phd=Christ’s College,1990-05 216||Exploiting OR-parallelism in Prolog using multiple sequential machines|Carole Susan Klein |250|phd=Wolfson College,1989-10 217||Dynamic bandwidth management|Bhaskar Ramanathan Harita |160|phd=Wolfson College,1990-10 218|1991-04|Higher-order critical pairs|Tobias Nipkow |15| 219|1991-03|Fairisle project working documents\\Snapshot 1|Ian M. Leslie , Derek M. McAuley , Mark Hayter , Richard Black , Reto Beller, Peter Newman , Matthew Doar |56| 220||A distributed architecture for multimedia communication systems|Cosmos Andrea Nicolaou |192|phd=Christ’s College,1990-12 221||Transforming axioms for data types into sequential programs|Robert Milne|44| 222||Extensions to coloured petri nets and their application to protocols|Jonathan Billington|190|phd=Clare Hall,1990-05 223|1991-05|Shallow processing and automatic summarising: a first study|Philip Gladwin, Stephen Pulman , Karen Spärck Jones |65| 224||Generalised probabilistic LR parsing of natural language (corpora) with unification-based grammars|Ted Briscoe , John Carroll |45| 225|1991-05|Categorical multirelations, linear logic and petri nets (draft)|Valeria de Paiva |29| 226|1991-06|A new approach for improving system availability|Kwok-yan Lam |108|phd=Churchill College,1991-01 227|1991-06|Priority in process calculi|Juanito Albert Camilleri |203|phd=Trinity College,1990-10 228|1991-05|The desk area network|Mark Hayter , Derek McAuley |11| 229|1991-08|Abstraction of image and pixel\\The thistle display system|David J. Brown|197|phd=St John’s College,1991-02 230|1991-08|Proceedings of the Second Belief Representation and Agent Architectures Workshop (BRAA ’91)|J. Galliers|255| 231|1991-08|Managing the order of transactions in widely-distributed data systems|Raphael Yahalom |133|phd=Jesus College,1990-10 232|1991-07|Mechanising set theory|Francisco Corella|217|phd=Corpus Christi College,1989-06 233|1991-07|A development environment for large natural language grammars|John Carroll , Ted Briscoe , Claire Grover|65| 234|1991-08|Two tutorial papers:\\Information retrieval & Thesaurus|Karen Spärck Jones |31| 235||Modelling and image generation|Heng Wang |145|phd=St John’s College,1991-07 236||Using knowledge of purpose and knowledge of structure as a basis for evaluating the behaviour of mechanical systems|John Anthony Bradshaw |153|phd=Gonville & Caius College,1991-06 237||Computing presuppositions in an incremantal language processing system|Derek G. Bridge|212|phd=Wolfson College,1991-04 238|1991-10|Proceedings of the ACQUILEX Workshop on Default Inheritance in the lexicon|Ted Briscoe , Ann Copestake , Valeria de Paiva |180| 239|1991-12|Planning multisentential English text using communicative acts|Mark Thomas Maybury |329|phd=Wolfson College,1991-07 240|1991-12|Symbolic compilation and execution of programs by proof: a case study in HOL|Juanito Camilleri |31| 241|1991-12|Learning in large state spaces with an application to biped robot walking|Thomas Ulrich Vogel |204|phd=Wolfson College,1991-11 242|1992-01|An object-oriented approach to virtual memory management|Glenford Ezra Mapp |150|phd=Clare Hall,1991-09 243|1992-01|Automating the librarian: a fundamental approach using belief revision|Alison Cawsey, Julia Galliers, Steven Reece, Karen Spärck Jones |39| 244|1992-01|A mechanized theory of the π-calculus in HOL|T.F. Melham |31| 245|1992-01|System support for multi-service traffic|Michael J. Dixon |108|phd=Fitzwilliam College,1991-09 246|1992-02|A relevance-based utterance processing system|Victor Poznański |295|phd=Girton College,1990-12 247|1992-02|Programming metalogics with a fixpoint type|Roy Luis Crole |164|phd=Churchill College,1992-01 248|1992-02|On efficiency in theorem provers which fully expand proofs into primitive inferences|Richard J. Boulton |23| 249|1992-03|A formalisation of the VHDL simulation cycle|John P. Van Tassel |24| 250|1992-04|TouringMachines: autonomous agents with attitudes|Innes A. Ferguson |19| 251|1992-04|Multipoint digital video communications|Xiaofeng Jiang |124|phd=Wolfson College,1991-12 252||A co-induction principle for recursively defined domains|Andrew M. Pitts |25| 253||The (other) Cambridge ACQUILEX papers|Antonio Sanfilippo|141| 254|1992-04|A HOL semantics for a subset of ELLA|Richard J. Boulton |104| 255|1992|The formal verification of hard real-time systems|Rachel Mary Cardell-Oliver |151|phd=Queens’ College,1992-01 256|1992-05|MCPL programming manual|Martin Richards |32| 257|1992-05|Cut-free sequent and tableau systems for propositional normal modal logics|Rajeev Prakhakar Goré |160| 258|1992-05|Two papers on ATM networks|David J. Greaves , Derek McAuley , Leslie J. French|22| 259||Full abstraction in the Lazy Lambda Calculus|Samson Abramsky, C.-H. Luke Ong |104| 260|1992-06|Local computation of alternating fixed-points|Henrik Reif Anderson|21| 261|1992-08|Image resampling|Neil Anthony Dodgson |264|phd=Wolfson College, 262|1992-08|Term assignment for intuitionistic linear logic (preliminary report)|Nick Benton , Gavin Bierman , Valeria de Paiva |57| 263|1992-08|The Lazy Lambda Calculus:\\an investigation into the foundations of functional programming|C.-H. Luke Ong |256|ophd=Imperial College London,1988-05 264|1992-08|CCS with environmental guards|Juanito Camilleri |19| 265|1992-08|Reasoning with inductively defined relations in the HOL theorem prover|Juanito Camilleri , Tom Melham |49| 266|1992-09|Automatic exploitation of OR-parallelism in Prolog|Carole Klein |18| 267|1992-10|Untyped strictness analysis|Christine Ernoult, Alan Mycroft |13| 268|1992-10|Network file server design for continuous media|Paul W. Jardetzky|101|phd=Darwin College,1992-08 269|1992-10|Optimising compilation|Alan Mycroft , Arthur Norman |23| 270||Designing a universal name service|Chaoying Ma |133|phd=Newnham College,1992-10 271|1992-11|Set theory as a computational logic: I. from foundations to functions|Lawrence C. Paulson |28| 272|1992-11|Interactive program derivation|Martin David Coen |100|phd=St John’s College,1992-03 273|1992-11|TouringMachines:\\an architecture for dynamic, rational, mobile agents|Innes A. Ferguson |206|phd=Clare Hall,1992-10 274|1992-11|Of what use is a verified compiler specification?|Paul Curzon |23| 275||Exploratory learning in the game of GO|Barney Pell |18| 276||METAGAME: a new challenge for games and learning|Barney Pell |15| 277||METAGAME in symmetric chess-like games|Barney Pell |30| 278||A formalization of the process algebra CCS in high order logic|Monica Nesi |42| 279|1992-12|The transition assertions specification method|Victor A. Carreño|18| 280|1993-01|Introduction to Isabelle|Lawrence C. Paulson |61| 281|1992-09|Pegasus project description|Sape J. Mullender, Ian M. Leslie , Derek McAuley |23| 282|1992-12|Pegasus – Operating system support for distributed multimedia systems|Ian M. Leslie , Derek McAuley , Sape J. Mullender|14| 283|1993-02|The Isabelle reference manual|Lawrence C. Paulson |78| 284|1993-01|The Alvey Natural Language Tools grammar (4th Release)|Claire Grover, John Carroll , Ted Briscoe |260| 285|1993-02|Functional programming and input/output|Andrew Donald Gordon |163|phd=King’s College,1992-08 286|1993-02|Isabelle’s object-logics|Lawrence C. Paulson |161| 287|1993-02|A mechanised definition of Silage in HOL|Andrew D. Gordon |28| 288|1993-02|Cut-free sequent and tableau systems for propositional Diodorean modal logics|Rajeev Gore |19| 289|1993-02|The semantics of noun phrase anaphora|David Alan Howard Elworthy |191|phd=Darwin College,1993-02 290|1993-02|Discourse modelling for automatic summarising|Karen Spärck Jones |30| 291|1993-02|Evaluating natural language processing systems|J.R. Galliers, K. Spärck Jones |187| 292|1993-03|Synchronisation services for digital continuous media|Cormac John Sreenan |123|phd=Christ’s College,1992-10 293|1993-04|Objects and transactions for modelling distributed applications:\\concurrency control and commitment|Jean Bacon , Ken Moody |39| 294|1993-04|OPERA\\Storage, programming and display of multimedia objects|Ken Moody , Jean Bacon , Noha Adly , Mohamad Afshar , John Bates, Huang Feng, Richard Hayton , Sai Lai Lo , Scarlet Schwiderski , Robert Sultana , Zhixue Wu |9| 295|1993-04|OPERA\\Storage and presentation support for multimedia applications in a distributed, ATM network environment|Jean Bacon , John Bates, Sai Lai Lo , Ken Moody |12| 296|1993-04|A persistent programming language for multimedia databases in the OPERA project|Z. Wu , K. Moody , J. Bacon |9| 297|1993-04|Categorical abstract machines for higher-order typed lambda calculi|Eike Ritter |149|phd=Trinity College, 298|1993-04|Multicast in the asynchronous transfer mode environment|John Matthew Simon Doar |168|phd=St John’s College,1993-01 299|1993-04|Pragmatic reasoning in bridge|Bjorn Gamback, Manny Rayner, Barney Pell |23| 300|1993-04|Formal verification of VIPER’s ALU|Wai Wong|78| 301|1993-06|The dual-level validation concurrency control method|Zhixue Wu , Ken Moody , Jean Bacon |24| 302|1993-06|Logic programming for general game-playing|Barney Pell |15| 303|1993-06|Drawing trees —\\a case study in functional programming|Andrew Kennedy|9| 304|1993-07|Co-induction and co-recursion in higher-order logic|Lawrence C. Paulson |35| 305|1993-07|Strong normalisation for the linear term calculus|P.N. Benton |13| 306|1993-07|Recording HOL proofs|Wai Wong|57| 307|1993-07|Natural language processing for information retrieval|David D. Lewis, Karen Spärck Jones |22| 308|1993-08|A case study of co-induction in Isabelle HOL|Jacob Frost|27| 309|1993-08|Strictness analysis of lazy functional programs|Peter Nicholas Benton |154|phd=Pembroke College,1992-12 310|1993-08|HARP: a hierarchical asynchronous replication protocol for massively replicated systems|Noha Adly |34| 311|1993-09|A verified Vista implementation|Paul Curzon |56| 312|1993-09|Set theory for verification: II\\Induction and recursion|Lawrence C. Paulson |46| 313|1993-10|Proof by pointing|Yves Bertot, Gilles Kahn, Laurent Théry|27| 314||Practical unification-based parsing of natural language|John Andrew Carroll |173|phd=,1993-09 315|1993-11|Strategy generation and evaluation for meta-game playing|Barney Darryl Pell |289|phd=Trinity College,1993-08 316|1993-08|The Compleat LKB|Ann Copestake |126| 317|1993-11|Femto-VHDL:\\the semantics of a subset of VHDL and its embedding in the HOL proof assistant|John Peter Van Tassel |122|phd=Gonville & Caius College,1993-07 318|1993-11|A method of program refinement|Jim Grundy |207|phd=Fitzwilliam College,1993-11 319|1993-11|A workstation architecture to support multimedia|Mark David Hayter |99|phd=St John’s College,1993-09 320|1995-07|A fixedpoint approach to implementing (co)inductive definitions (updated version)|Lawrence C. Paulson |29| 321|1993-12|Relational properties of domains|Andrew M. Pitts |38| 322|1993-12|Supporting distributed realtime computing|Guangxing Li |113|phd=King’s College,1993-08 323|1994-01|Representing higher-order logic proofs in HOL|J. von Wright|28| 324|1994-01|Verifying modular programs in HOL|J. von Wright|25| 325|1994-01|The temporal properties of English conditionals and modals|Richard Crouch |248|phd=,1993-04 326|1994-01|A modular and extensible network storage architecture|Sai-Lai Lo |147|phd=Darwin College,1993-11 327|1994-02|A new application for explanation-based generalisation within automated deduction|Siani L. Baker|18| 328|1994-03|The formal verification of the Fairisle ATM switching element: an overview|Paul Curzon |46| 329|1994-03|The formal verification of the Fairisle ATM switching element|Paul Curzon |105| 330|1994-03|Interacting with paper on the DigitalDesk|Pierre David Wellner |96|phd=Clare Hall,1993-10 331|1994-03|HPP: a hierarchical propagation protocol for large scale replication in wide area networks|Noha Adly , Akhil Kumar|24| 332|1994-03|Distributed computing with objects|David Martin Evers |154|phd=Queens’ College,1993-09 333|1994-04|What is a categorical model of intuitionistic linear logic?|G.M. Bierman |15| 334|1994-05|A concrete final coalgebra theorem for ZF set theory|Lawrence C. Paulson |21| 335|1994-04|Video mail retrieval using voice: report on keyword definition and data collection (deliverable report on VMR task No. 1)|G.J.F. Jones , J.T. Foote, K. Spärck Jones , S.J. Young |38| 336|1994-05|Towards a proof theory of rewriting: the simply-typed 2-λ calculus|Barnaby P. Hilken|28| 337|1994-05|Efficiency in a fully-expansive theorem prover|Richard John Boulton |126|phd=Churchill College,1993-12 338|1994-05|A new approach to implementing atomic data types|Zhixue Wu |170|phd=Trinity College,1993-10 339|1994-05|Belief revision and dialogue management in information retrieval|Brian Logan, Steven Reece, Alison Cawsey, Julia Galliers, Karen Spärck Jones |227| 340|1994-06|Operating system support for quality of service|Eoin Andrew Hyden |102|phd=Wolfson College,1994-02 341|1994-06|Presentation support for distributed multimedia applications|John Bates|140| 342|1994-07|An architecture for distributed user interfaces|Stephen Martin Guy Freeman |127|phd=Darwin College,1994 343|1994-07|An investigation of real-time synchronisation|Akira Nakamura |134|phd=Wolfson College,1993-12|deleted=,removed by supervisor Roger Needham 344|1994-07|The contour tree image encoding technique and file format|Martin John Turner |154|phd=St John’s College,1994-04 345|1994-08|A proof environment for arithmetic with the Omega rule|Siani L. Baker|17| 346|1994-08|On intuitionistic linear logic|G.M. Bierman |191|phd=Wolfson College,1993-12 347|1994-07|Reflections on TREC|Karen Spärck Jones |35| 348|1994-08|Integrated sound synchronisation for computer animation|Jane Louise Hunter |248|phd=Newnham College,1994-08 349|1994-09|A HOL interpretation of Noden|Brian Graham |78| 350|1994-09|Ten commandments of formal methods|Jonathan P. Bowen, Michael G. Hinchey |18| 351|1994-09|Handling realtime traffic in mobile networks|Subir Kumar Biswas |198|phd=Darwin College,1994-08 352|1994-10|A mixed linear and non-linear logic: proofs, terms and models|P.N. Benton |65| 353|1994-11|Merging HOL with set theory|Mike Gordon |40| 354|1994-11|Formalising a model of the λ-calculus in HOL-ST|Sten Agerholm|31| 355|1994-11|Two cryptographic notes|David Wheeler , Roger Needham |6| 356|1994-12|Simple, proven approaches to text retrieval|S.E. Robertson, K. Spärck Jones |8|updated=1996-05,1997-05,2006-02 357|1994-12|Seven more myths of formal methods|Jonathan P. Bowen, Michael G. Hinchey |12| 358|1995-02|Multithreaded processor design|Simon William Moore |125|phd=Trinity Hall,1994-10|front=This report was also published as a book of the same title (Kluwer/Springer-Verlag, 1996, ISBN 0-7923-9718-5). 359|1995-02|A case study of co-induction in Isabelle|Jacob Frost|48| 360|1995-03|On the calculation of explicit polymetres|W.F. Clocksin |12| 361|1995-04|Explicit network scheduling|Richard John Black |121|phd=Churchill College,1994-12 362|1995-04|W-learning:\\competition among selfish Q-learners|Mark Humphrys |30| 363|1995-04|Names and higher-order functions|Ian Stark |140|phd=Queens’ College,1994-12 364|1995-04|The Church-Rosser theorem in Isabelle:\\a proof porting experiment|Ole Rasmussen|27| 365|1995-05|Computational types from a logical perspective I|P.N. Benton , G.M. Bierman , V.C.V. de Paiva |19| 366|1995-05|Retrieving spoken documents: VMR Project experiments|K. Spärck Jones , G.J.F. Jones , J.T. Foote, S.J. Young |28| 367|1995-05|Categorical logic|Andrew M. Pitts |94| 368|1995-06|CogPiT – configuration of protocols in TIP|Burkhard Stiller|73| 369|1995-07|A comparison of HOL-ST and Isabelle/ZF|Sten Agerholm|23| 370|1995-07|A package for non-primitive recursive function definitions in HOL|Sten Agerholm|36| 371|1995-06|LIMINF convergence in Ω-categories|Kim Ritter Wagner|28| 372|1995-01|A brief history of mobile telephony|Stefan G. Hild |19| 373|1995-07|Natural-language processing and requirements specifications|Benjamín Macías, Stephen G. Pulman |73| 374|1995-07|A framework for QoS updates in a networking environment|Burkhard Stiller|| 375|1995-07|Restructuring virtual memory to support distributed computing environments|Feng Huang |145|phd=Clare Hall,1995-07 376|1995-08|The structure of a multi-service operating system|Timothy Roscoe |113|phd=Queens’ College,1995-04 377|1995-07|Mechanising set theory: cardinal arithmetic and the axiom of choice|Larry Paulson , Krzysztof Grabczewski|33| 378|1995-08|Performance evaluation of HARP: a hierarchical asynchronous replication protocol for large scale system|Noha Adly |94| 379|1995-09|Proceedings of the First Isabelle Users Workshop|Lawrence Paulson |265| 380|1995-09|Quality-of-Service issues in networking environments|Burkhard Stiller|68| 381|1995-10|Rendering for free form deformations|Uwe Michael Nimscheck |151|phd=Wolfson College, 382|1995-10|Synthetic image generation for a multiple-view autostereo display|Oliver M. Castle |184|phd=Wolfson College,1995-04 383|1995-11|Management of replicated data in large scale systems|Noha Adly |182|phd=Corpus Christi College,1995-08 384|1995-01|Securing ATM networks|Shaw-Cheng Chuang |30| 385|1995-12|Performance evaluation of the Delphi machine|Sanjay Saraswat |187|phd=St Edmund’s College,1995-10 386|1996-01|Bisimilarity for a first-order calculus of objects with subtyping|Andrew D. Gordon , Gareth D. Rees |78| 387|1996-02|Monitoring composite events in distributed systems|Scarlet Schwiderski , Andrew Herbert, Ken Moody |20| 388|1996-02|A unified approach to strictness analysis and optimising transformations|P.N. Benton |21| 389|1996-03|A proof checked for HOL|Wai Wong|165| 390|1996-03|Syn: a single language for specifiying abstract syntax tress, lexical analysis, parsing and pretty-printing|Richard J. Boulton |25| 391|1996-04|Programming languages and dimensions|Andrew John Kennedy |149|phd=St Catherine’s College,1995-11 392|1996-04|Decoding choice encodings|Uwe Nestmann, Benjamin C. Pierce|54| 393|1996-04|Performance management in ATM networks|Simon Andrew Crosby |215|phd=St John’s College,1995-05 394|1996-04|A simple formalization and proof for the mutilated chess board|Lawrence C. Paulson |11| 395|1996-05|Cut-elimination for full intuitionistic linear logic|Torben Bräuner, Valeria de Paiva |27| 396|1996-05|Generic automatic proof tools|Lawrence C. Paulson |28| 397|1996-06|Optimal routing in 2-jump circulant networks|Borut Robič|7| 398|1996-06|Design and implementation of an autostereoscopic camera system|N.A. Dodgson , J.R. Moore|20| 399|1996-06|OASIS:\\An open architecture for secure interworking services|Richard Hayton |102|phd=Fitzwilliam College,1996-03 400|1996-07|Monitoring the behaviour of distributed systems|Scarlet Schwiderski |161|phd=Selwyn College,1996-04 401|1996-07|A classical linear λ-calculus|Gavin Bierman |41| 402|1996-09|Video mail retrieval using voice: report on collection of naturalistic requests and relevance assessments|G.J.F. Jones , J.T. Foote, K. Spärck Jones , S.J. Young |21| 403|1996-10|Devices in a multi-service operating system|Paul Ronald Barham |131|phd=Churchill College,1996-06 404|1996-11|Adaptive parallelism for computing on heterogeneous clusters|Kam Hong Shum |147|phd=Darwin College,1996-08 405|1996-11|A tool to support formal reasoning about computer languages|Richard J. Boulton |21| 406|1996-11|Tool support for logics of programs|Lawrence C. Paulson |31| 407|1996-09|The L4 microkernel on Alpha\\Design and implementation|Sebastian Schoenberg|51| 408|1996-11|Theorem proving with the real numbers|John Robert Harrison |147|phd=Churchill College,1996-06 409|1996-12|Proving properties of security protocols by induction|Lawrence C. Paulson |24| 410|1997-01|Proof style|John Harrison |22| 411|1997-01|Formalising process calculi in Higher Order Logic|Monica Nesi |182|phd=Girton College,1996-04 412|1997-01|Observations on a linear PCF (preliminary report)|G.M. Bierman |30| 413|1997-01|Mechanized proofs of security protocols:\\Needham-Schroeder with public keys|Lawrence C. Paulson |20| 414|1997-01|A calculus for cryptographic protocols\\The SPI calculus|Martín Abadi, Andrew D. Gordon |105| 415|1997-02|Application support for mobile computing|Steven Leslie Pope |145|phd=Jesus College,1996-10 416|1997-02|DECLARE: a prototype declarative proof system for higher order logic|Donald Syme |25| 417|1997-02|Selective mesh refinement for interactive terrain rendering|Peter J.C. Brown |18| 418|1997-03|Mechanized proofs for a recursive authentication protocol|Lawrence C. Paulson |30| 419|1997-04|Video-augmented environments|James Quentin Stafford-Fraser |91|phd=Gonville & Caius College,1996-02 420|1997-04|Managing complex models for computer graphics|Jonathan Mark Sewell |206|phd=Queens’ College,1996-03 421|1997-05|An abstract dynamic semantics for C|Michael Norrish |31| 422|1997-05|Using the BONITA primitives: a case study|Antony Rowstron|19| 423|1997-05|Symbol grounding:\\Learning categorical and sensorimotor predictions for coordination in autonomous robots|Karl F. MacDorman |170|phd=Wolfson College,1997-03 424|1997-05|Simplification with renaming:\\a general proof technique for tableau and sequent-based provers|Fabio Massacci|26| 425|1997-05|Should your specification language be typed?|Leslie Lamport, Lawrence C. Paulson |30| 426|1997-06|Action selection methods using reinforcement learning|Mark Humphrys |195|phd=Trinity Hall, 427|1997-06|Proving Java type soundness|Don Syme |35| 428|1997-06|Floating point verification in HOL Light: the exponential function|John Harrison |112| 429|1997-06|Compilation and equivalence of imperative objects|Andrew D. Gordon , Paul D. Hankin , Søren B. Lassen|64| 430|1997-07|Video mail retrieval using voice:\\Report on topic spotting\\(Deliverable report on VMR task no. 6)|G.J.F. Jones , J.T. Foote, K. Sparck Jones , S.J. Young |73| 431|1997-07|The MCPL programming manual and user guide|Martin Richards |70| 432|1997-07|On two formal analyses of the Yahalom protocol|Lawrence C. Paulson |16| 433|1997-07|Backtracking algorithms in MCPL using bit patterns and recursion|Martin Richards |80| 434|1997-08|Demonstration programs for CTL and μ-calculus symbolic model checking|Martin Richards |41| 435|1997-08|Global/local subtyping for a distributed π-calculus|Peter Sewell |57| 436|1997-11|A new method for estimating optical flow|W.F. Clocksin |20| 437|1997-12|Trusting in computer systems|William S. Harbison |95|phd=Wolfson College,1997-05 438|1997-11|An architecture for scalable and deterministic video servers|Feng Shi |148|phd=Wolfson College,1997-06 439|1997-12|Applying mobile code to distributed systems|David A. Halls |158|phd=,1997-06 440|1997-12|Inductive analysis of the internet protocol TLS|Lawrence C. Paulson |19| 441|1998-01|A generic tableau prover and its integration with Isabelle|Lawrence C. Paulson |16| 442|1998-01|A combination of nonstandard analysis and geometry theorem proving, with application to Newton’s Principia|Jacques Fleuriot , Lawrence C. Paulson |13| 443|1998-02|The inductive approach to verifying cryptographic protocols|Lawrence C. Paulson |46| 444|1998-05|From rewrite rules to bisimulation congruences|Peter Sewell |72| 445|1998-07|Secure sessions from weak secrets|Michael Roe , Bruce Christianson , David Wheeler |12| 446|1998-08|A probabilistic model of information and retrieval:\\development and status|K. Spärck Jones , S. Walker, S.E. Robertson|74| 447|1998-09|Are timestamps worth the effort?\\A formal treatment|Giampaolo Bella , Lawrence C. Paulson |12| 448|1998-09|A computational interpretation of the λμ calculus|G.M. Bierman |10| 449|1998-10|Locales\\A sectioning concept for Isabelle|Florian Kammüller , Markus Wenzel|16| 450|1998-11|Open service support for ATM|Jacobus Erasmus van der Merwe |164|phd=St John’s College,1997-09 451|1998-11|The structure of open ATM control architectures|Sean Rooney |183|phd=Wolfson College,1998-02 452|1998-11|A formal proof of Sylow’s theorem\\An experiment in abstract algebra with Isabelle Hol|Florian Kammüller , Lawrence C. Paulson |30| 453|1998-12|C formalised in HOL|Michael Norrish |156|phd=,1998-08 454|1998-12|Parametric polymorphism and operational equivalence|Andrew M. Pitts |39| 455|1998-12|Multiple modalities|G.M. Bierman |26| 456|1999-01|An evaluation based approach to process calculi|Joshua Robert Xavier Ross |206|phd=Clare College,1998-07 457|1999-02|A concurrent object calculus:\\reduction and typing|Andrew D. Gordon , Paul D. Hankin |63| 458|1999-03|Final coalgebras as greatest fixed points in ZF set theory|Lawrence C. Paulson |25| 459|1999-07|An open parallel architecture for data-intensive applications|Mohamad Afshar |225|phd=King’s College,1998-12 460|1999-03|Message reception in the inductive approach|Giampaolo Bella |16| 461|1999-03|Integrating Gandalf and HOL|Joe Hurd |11| 462|1999-04|Location-independent communication for mobile agents: a two-level architecture|Peter Sewell , Paweł T. Wojciechowski , Benjamin C. Pierce|31| 463|1999-04|Secure composition of insecure components|Peter Sewell , Jan Vitek|44| 464|1999-05|Feature representation for the automatic analysis of fluorescence in-situ hybridization images|Boaz Lerner , William Clocksin , Seema Dhanjal, Maj Hultén, Christipher Bishop|36| 465|1999-05|Gelfish – graphical environment for labelling FISH images|Boaz Lerner , Seema Dhanjal, Maj Hultén|20| 466|1999-05|Automatic signal classification in fluorescence in-situ hybridization images|Boaz Lerner , William Clocksin , Seema Dhanjal, Maj Hultén, Christipher Bishop|24| 467|1999-06|Mechanizing UNITY in Isabelle|Lawrence C. Paulson |22| 468|1999-07|Synthesis of asynchronous circuits|Stephen Paul Wilcox |250|phd=Queens’ College,1998-12 469|1999-08|A combination of geometry theorem proving and nonstandard analysis, with application to Newton’s Principia|Jacques Désiré Fleuriot |135|phd=Clare College,1999-03 470|1999-08|Modular reasoning in Isabelle|Florian Kammüller |128|phd=Clare College,1999-04 471|1999-09|Murphy’s law, the fitness of evolving species, and the limits of software reliability|Robert M. Brady , Ross J. Anderson , Robin C. Ball|14| 472|1999-09|Simulating music learning with autonomous listening agents: entropy, ambiguity and context|Ben Y. Reis |200|phd=Queens’ College,1999-07 473|1999-10|Computer algebra and theorem proving|Clemens Ballarin |122|phd=Darwin College, 474|1999-10|A Bayesian methodology and probability density estimation for fluorescence in-situ hybridization signal classification|Boaz Lerner |31| 475|1999-10|A comparison of state-of-the-art classification techniques with application to cytogenetics|Boaz Lerner , Neil D. Lawrence |34| 476|1999-11|Linking ACL2 and HOL|Mark Staples |23| 477|1999-11|Presheaf models for CCS-like languages|Gian Luca Cattani , Glynn Winskel |46| 478|1999-11|Secure composition of untrusted code: wrappers and causality types|Peter Sewell , Jan Vitek|36| 479|1999-12|The interaction between fault tolerance and security|Geraint Price |144|phd=Wolfson College,1999-06 480|1999-12|Programming combinations of deduction and BDD-based symbolic calculation|Mike Gordon |24| 481|1999-12|Combining the Hol98 proof assistant with the BuDDy BDD package|Mike Gordon , Ken Friis Larsen |71| 482|2000-01|Biometric decision landscapes|John Daugman |15| 483|2000-01|Elastic network control|Hendrik Jaap Bos |184|phd=Wolfson College,1999-08 484|2000-01|Automatic summarising and the CLASP system|Richard Tucker |190|phd=,1999 485|2000-01|Three notes on the interpretation of Verilog|Daryl Stewart , Myra VanInwegen |47| 486|2000-02|Stretching a point: aspect and temporal discourse|James Richard Thomas |251|phd=Wolfson College,1999-01 487|2000-03|Sequential program composition in UNITY|Tanja Vos, Doaitse Swierstra|20| 488|2000-03|Formal verification of card-holder registration in SET|Giampaolo Bella , Fabio Massacci, Lawrence Paulson , Piero Tramontano|15| 489|2000-04|Designing a reliable publishing framework|Jong-Hyeon Lee |129|phd=Wolfson College,2000-01 490|2000-04|Selective mesh refinement for rendering|Peter John Cameron Brown |179|phd=Emmanuel College,1998-02 491|2000-05|Is hypothesis testing useful for subcategorization acquisition?|Anna Korhonen , Genevive Gorrell, Diana McCarthy|9| 492|2000-06|Nomadic Pict: language and infrastructure design for mobile computation|Paweł Tomasz Wojciechowski |184|phd=Wolfson College,2000-03 493|2000-07|Inductive verification of cryptographic protocols|Giampaolo Bella |189|phd=Clare College,2000-03 494|2000-07|An architecture for the notification, storage and retrieval of events|Mark David Spiteri |165|phd=Darwin College,2000-01 495|2000-07|Automatic recognition of words in Arabic manuscripts|Mohammad S.M. Khorsheed |242|phd=Churchill College,2000-06 496|2000-07|Contexts and embeddings for closed shallow action graphs|Gian Luca Cattani , James J. Leifer , Robin Milner |56| 497|2000-09|Towards a formal type system for ODMG OQL|G.M. Bierman , A. Trigoni |20| 498|2000-07|Applied π – a brief tutorial|Peter Sewell |65| 499|2000-08|Enhancing spatial deformation for virtual sculpting|James Edward Gain |161|phd=St John’s College,2000-06|back=Pages ii–iv and vi have been removed from this Technical Report to save space; they contained only a formal declaration relating to the PhD submission or were blank. 500|2000-09|The memorability and security of passwords – some empirical results|Jianxin Yan , Alan Blackwell , Ross Anderson , Alasdair Grant|13| 501|2000-09|Integrated quality of service management|David Ingram |90|phd=Jesus College,2000-08 502|2000-09|Formalizing basic number theory|Thomas Marthedal Rasmussen |20| 503|2000-09|Hardware/software co-design using functional languages|Alan Mycroft , Richard Sharp |8| 504|2000-09|Word sense selection in texts: an integrated model|Oi Yee Kwong |177|phd=Downing College,2000-05 505|2000-09|Models for name-passing processes: interleaving and causal|Gian Luca Cattani , Peter Sewell |42| 506|2000-09|Modules, abstract types, and distributed versioning|Peter Sewell |46| 507|2000-11|Mechanizing a theory of program composition for UNITY|Lawrence Paulson |28| 508|2000-10|Shallow linear action graphs and their embeddings|James Leifer , Robin Milner |16| 509|2001-01|Proximity visualisation of abstract data|Wojciech Basalaj |117|phd=,2000-10 510|2000-05|Switchlets and resource-assured MPLS networks|Richard Mortier , Rebecca Isaacs , Keir Fraser |16| 511|1999-12|Software visualization in Prolog|Calum Grant |193|phd=Queens’ College,1999 512|2001-03|An algebraic framework for modelling and verifying microprocessors using HOL|Anthony Fox |24| 513|2001-05|Generic summaries for indexing in information retrieval – Detailed test results|Tetsuya Sakai , Karen Spärck Jones |29| 514|2001-06|Nomadic π-calculi: expressing and verifying communication infrastructure for mobile computation|Asis Unyapoth |316|phd=Pembroke College,2001-03 515|2001-07|The UDP calculus:\\rigorous semantics for real networking|Andrei Serjantov , Peter Sewell , Keith Wansbrough |70| 516|2001-09|Dynamic provisioning of resource-assured and programmable virtual private networks|Rebecca Isaacs |145|phd=Darwin College,2000-12 517|2001-07|The Cambridge Multimedia Document Retrieval Project:\\summary of experiments|Karen Spärck Jones , P. Jourlin , S.E. Johnson, P.C. Woodland|30| 518|2001-07|An attack on a traitor tracing scheme|Jeff Jianxin Yan , Yongdong Wu|14| 519|2001-08|Local evidence in document retrieval|Martin Choquette |177|phd=Fitzwilliam College,2002-11 520|2001-09|Ternary and three-point univariate subdivision schemes|Mohamed Hassan , Neil A. Dodgson |8| 521|2001-09|Operational congruences for reactive systems|James Leifer |144|phd=Trinity College,2001-03 522|2001-09|Practical behavioural animation based on vision and attention|Mark F.P. Gillies |187| 523|2001-09|Bigraphical reactive systems: basic theory|Robin Milner |87| 524|2001-11|Verifying the SET purchase protocols|Giampaolo Bella , Fabio Massacci, Lawrence C. Paulson |14| 525|2001-12|Extensible virtual machines|Timothy L. Harris |209|phd 526|2001-12|Extending lossless image compression|Andrew J. Penrose |137|phd=Gonville & Caius College,2001-01 527|2002-01|Architectures for ubiquitous systems|Umar Saif |271|phd 528|2002-04|Measurement-based management of network resources|Andrew William Moore |273|phd 529|2002-02|The triVM intermediate language reference manual|Neil Johnson |83|front=This research was sponsored by a grant from ARM Limited. 530|2002-02|Subcategorization acquisition|Anna Korhonen |189|phd=Trinity Hall,2001-09 531|2002-03|Verifying the SET registration protocols|Giampaolo Bella , Fabio Massacci, Lawrence C. Paulson |24| 532|2002-04|Internet traffic engineering|Richard Mortier |129|phd=Churchill College,2001-10 533|2002-04|The acquisition of a unification-based generalised categorial grammar|Aline Villavicencio |223|phd=Hughes Hall,2001-09|back=The thesis was partially sponsored by a doctoral studentship from CAPES/Brazil. 534|2002-04|Resource control in network elements|Austin Donnelly |183|phd=Pembroke College,2002-01 535|2002-05|Designs, disputes and strategies|Claudia Faggian, Martin Hyland|21| 536|2002-06|Low temperature data remanence in static RAM|Sergei Skorobogatov |9| 537|2002-06|Parallel systems in symbolic and algebraic computation|Mantsika Matooane |139|phd=Trinity College,2001-08 538|2002-06|The Escritoire: A personal projected display for interacting with documents|Mark Ashdown , Peter Robinson |12| 539|2002-07|Towards a ternary interpolating subdivision scheme for the triangular mesh|N.A. Dodgson , M.A. Sabin , L. Barthe , M.F. Hassan |12| 540|2002-08|The use of computer graphics rendering software in the analysis of a novel autostereoscopic display design|N.A. Dodgson , J.R. Moore|6| 541|2002-08|Different applications of two-dimensional potential fields for volume modeling|L. Barthe , N.A. Dodgson , M.A. Sabin , B. Wyvill, V. Gaildrat|26| 542|2002-09|A generative classification of mesh refinement rules with lattice transformations|I.P. Ivrissimtzis , N.A. Dodgson , M.A. Sabin |13|front=An updated, improved version of this report has been published in Computer Aided Geometric Design 22(1):99–109, January 2004 [doi:10.1016/j.cagd.2003.08.001]. The classification scheme is slightly different in the CAGD version. Please refer to the CAGD version in any work which you produce. 543|2002-09|Evaluating similarity-based visualisations as interfaces for image browsing|Kerry Rodden |248|phd=Newnham College,2001-10-11|colour 544|2002-09|On the support of recursive subdivision|I.P. Ivrissimtzis , M.A. Sabin , N.A. Dodgson |20|front=An updated, improved version of this report has been published in ACM Trans. Graphics 23(4):1043–1060, October 2004 [doi:10.1145/1027411.1027417] 545|2001-06|A HOL specification of the ARM instruction set architecture|Anthony C.J. Fox |45| 546|2002-09|Depth perception in computer graphics|Jonathan David Pfautz |182|phd=Trinity College,2000-05 547|2002-10|Semantic optimization of OQL queries|Agathoniki Trigoni |171|phd=Pembroke College,2001-10 548|2002-11|Formal verification of the ARM6 micro-architecture|Anthony Fox |59| 549|2002-12|Two remarks on public key cryptology|Ross Anderson |7| 550|2002-06|Computer security –\\a layperson’s guide, from the bottom up|Karen Spärck Jones |23| 551|2002-12|The relative consistency of the axiom of choice —\\mechanized using Isabelle/ZF|Lawrence C. Paulson |63| 552|2003-01|The Xenoserver computing infrastructure|Keir A. Fraser , Steven M. Hand , Timothy L. Harris , Ian M. Leslie , Ian A. Pratt |11| 553|2003-01|Xen 2002|Paul R. Barham , Boris Dragovic , Keir A. Fraser , Steven M. Hand , Timothy L. Harris , Alex C. Ho , Evangelos Kotsovinos , Anil V.S. Madhavapeddy , Rolf Neugebauer, Ian A. Pratt , Andrew K. Warfield |15| 554|2003-01|Towards a field theory for networks|Jon Crowcroft |9| 555|2003-01|BOURSE – Broadband Organisation of Unregulated Radio Systems through Economics|Jon Crowcroft , Richard Gibbens , Stephen Hailes|10| 556|2003-01|Turing Switches – Turing machines for all-optical Internet routing|Jon Crowcroft |7| 557|2003-01|Iota: A concurrent XML scripting language with applications to Home Area Networking|G.M. Bierman , P. Sewell |32| 558|2003-01|A role and context based security model|Yolanta Beresnevichiene |89|phd=Wolfson College,2000-06 559|2003-02|Pronto: MobileGateway with publish-subscribe paradigm over wireless network|Eiko Yoneki , Jean Bacon |22| 560|2003-02|Decimalisation table attacks for PIN cracking|Mike Bond , Piotr Zieliński |14| 561|2003-03|Resource control of untrusted code in an open network environment|Paul B. Menage |185|phd=Magdalene College,2000-06|colour 562|2003-04|Fast Marching farthest point sampling|Carsten Moenning , Neil A. Dodgson |16| 563|2003-04|MJ: An imperative core calculus for Java and Java with effects|G.M. Bierman , M.J. Parkinson , A.M. Pitts |53| 564|2003-05|Access policies for middleware|Ulrich Lang |138|phd=Wolfson College,2003-03 565|2003-05|Fast Marching farthest point sampling for point clouds and implicit surfaces|Carsten Moenning , Neil A. Dodgson |15| 566|2003-05|Formal verification of probabilistic algorithms|Joe Hurd |154|phd=Trinity College,2001-12 567|2003-06|Using inequalities as term ordering constraints|Joe Hurd |17| 568|2004-02|Dynamic rebinding for marshalling and update, with destruct-time λ|Gavin Bierman , Michael Hicks , Peter Sewell , Gareth Stoyle , Keith Wansbrough |85| 569|2003-06|Global abstraction-safe marshalling with hash types|James J. Leifer , Gilles Peskine , Peter Sewell , Keith Wansbrough |86| 570|2003-07|Bigraphs and mobile processes|Ole Høgh Jensen , Robin Milner |121| 571|2003-07|Multi-layer network monitoring and analysis|James Hall |230|phd=King’s College,2003-04|colour 572|2003-08|Design choices for language-based transactions|Tim Harris |7| 573|2003-08|Mechanizing compositional reasoning for concurrent systems: some lessons|Lawrence C. Paulson |20| 574|2003-09|Sketchpad: A man-machine graphical communication system|Ivan Edward Sutherland|149|ophd=Massachusetts Institute of Technology,1963-01|contrib=new preface::Alan Blackwell , Kerry Rodden 575|2003-11|Reconfigurable wavelength-switched optical networks for the Internet core|Tim Granger |184|phd=King’s College,2003-08|colour 576|2003-11|An implementation of a coordinate based location system|David R. Spence |12| 577|2003-12|Compromising emanations: eavesdropping risks of computer displays|Markus G. Kuhn |167|phd=Wolfson College,2002-06 578|2004-01|Linear types for packet processing (extended version)|Robert Ennals , Richard Sharp , Alan Mycroft |31| 579|2004-02|Practical lock-freedom|Keir Fraser |116|phd=King’s College,2003-09 580|2004-02|Bigraphs and mobile processes (revised)|Ole Høgh Jensen , Robin Milner |131| 581|2004-02|Axioms for bigraphical structure|Robin Milner |26| 582|2004-02|Latency-optimal Uniform Atomic Broadcast algorithm|Piotr Zieliński |28| 583|2004-03|Subdivision as a sequence of sampled Cp surfaces and conditions for tuning schemes|Cédric Gérot, Loïc Barthe , Neil A. Dodgson , Malcolm A. Sabin |68| 584|2004-03|Concise texture editing|Stephen Brooks |164|phd=Jesus College,2003-10 585|2004-03|Personal projected displays|Mark S. D. Ashdown |150|phd=Churchill College,2003-09 586|2004-03|Role-based access control policy administration|András Belokosztolszki |170|phd=King’s College,2003-11 587|2004-04|Verification of asynchronous circuits|Paul Alexander Cunningham |174|phd=Gonville and Caius College,2002-01 588|2004-05|MulTEP: A MultiThreaded Embedded Processor|Panit Watcharawitch |190|phd=Newnham College,2003-11 589|2004-05|new-HOPLA — a higher-order process language with name generation|Glynn Winskel , Francesco Zappa Nardelli|16| 590|2004-06|Hermes: A scalable event-based middleware|Peter R. Pietzuch |180|phd=Queens’ College,2004-02 591|2004-06|Conversion of notations|Silas S. Brown |159|phd=St John’s College,2003-11 592|2004-06|Unwrapping the Chrysalis|Mike Bond , Daniel Cvrček, Steven J. Murdoch |15| 593|2004-06|Paxos at war|Piotr Zieliński |30| 594|2004-07|Designing and attacking anonymous communication systems|George Danezis |150|phd=Queens’ College,2004-01 595|2004-07|Representations of quantum operations, with applications to quantum cryptography|Pablo J. Arrighi |157|phd=Emmanuel College,2003-09-23 596|2004-08|Reconstructing I/O|Keir Fraser , Steven Hand , Rolf Neugebauer, Ian Pratt , Andrew Warfield , Mark Williamson |16| 597|2004-08|Syntactic simplification and text cohesion|Advaith Siddharthan |195|phd=Gonville and Caius College,2003-11 598|2004-08|Transition systems, link graphs and Petri nets|James J. Leifer , Robin Milner |64| 599|2004-08|Further analysis of ternary and 3-point univariate subdivision schemes|Mohamed F. Hassan |9| 600|2004-08|Trust for resource control: Self-enforcing automatic rational contracts between computers|Brian Ninham Shand |154|phd=Jesus College,2004-02|back=This research was supported by ICL, now part of Fujitsu, through the Computer Laboratory’s ICL studentship, and by the Overseas Research Students award scheme, the Cambridge Commonwealth Trust, and the SECURE EU consortium. 601|2004-09|Combining model checking and theorem proving|Hasan Amjad |131|phd=Trinity College,2004-03 602|2004-09|Model checking the AMBA protocol in HOL|Hasan Amjad |27| 603|2004-09|Bigraphs whose names have multiple locality|Robin Milner |15| 604|2004-10|On the anonymity of anonymity systems|Andrei Serjantov |162|phd=Queens’ College,2003-03 605|2004-10|Acute: High-level programming language design for distributed computation\\Design rationale and language definition|Peter Sewell , James J. Leifer , Keith Wansbrough , Mair Allen-Williams , Francesco Zappa Nardelli, Pierre Habouzit, Viktor Vafeiadis |193| 606|2004-11|Dynamic binary analysis and instrumentation|Nicholas Nethercote |177|phd=Trinity College,2004-11 607|2004-11|Code size optimization for embedded processors|Neil E. Johnson |159|phd=Robinson College,2004-05 608|2004-11|Trust management for widely distributed systems|Walt Yao |191|phd=Jesus College,2003-02 609|2004-12|Using camera-phones to interact with context-aware mobile services|Eleanor Toye , Anil Madhavapeddy , Richard Sharp , David Scott , Alan Blackwell , Eben Upton |23| 610|2004-12|Influence of syntax on prosodic boundary prediction|Tommy Ingulfsen |49|mphil-cstit=Churchill College,2004-07 611|2004-12|An heuristic analysis of the classification of bivariate subdivision schemes|Neil A. Dodgson |18| 612|2005-01|Location privacy in ubiquitous computing|Alastair R. Beresford |139|phd=Robinson College,2004-04 613|2005-01|Abstracting application-level security policy for ubiquitous computing|David J. Scott |186|phd=Robinson College,2004-09 614|2005-01|Pure bigraphs|Robin Milner |66| 615|2005-01|Global public computing|Evangelos Kotsovinos |229|phd=Trinity Hall,2004-11 616|2005-02|Dictionary characteristics in cross-language information retrieval|Donnla Nic Gearailt |158|phd=Gonville and Caius College,2003-02 617|2005-02|Pocket Switched Networks: Real-world mobility and its consequences for opportunistic forwarding|Augustin Chaintreau, Pan Hui , Jon Crowcroft , Christophe Diot, Richard Gass, James Scott |26| 618|2005-02|The Fresh Approach: functional programming with names and binders|Mark R. Shinwell |111|phd=Queens’ College,2004-12 619|2005-02|Operating system support for simultaneous multithreaded processors|James R. Bulpin |130|phd=King’s College,2004-09 620|2005-02|Middleware support for context-awareness in distributed sensor-driven systems|Eleftheria Katsiri |176|phd=Clare College,2005-01 621|2005-02|Fresh Objective Caml user manual|Mark R. Shinwell , Andrew M. Pitts |21| 622|2005-03|Cooperation and deviation in market-based resource allocation|Jörg H. Lepler |173|phd=St John’s College,2004-11 623|2005-03|Simple polymorphic usage analysis|Keith Wansbrough |364|phd=Clare Hall,2002-03|back=Subtract 20 from each page number in this report to obtain the corresponding page number in the dissertation. 624|2005-03|TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification\\Volume 1: Overview|Steve Bishop, Matthew Fairbairn , Michael Norrish , Peter Sewell , Michael Smith , Keith Wansbrough |88| 625|2005-03|TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification\\Volume 2: The Specification|Steve Bishop, Matthew Fairbairn , Michael Norrish , Peter Sewell , Michael Smith , Keith Wansbrough |386| 626|2005-03|Landmark Guided Forwarding: A hybrid approach for Ad Hoc routing|Meng How Lim , Adam Greenhalgh, Julian Chesterfield , Jon Crowcroft |28| 627|2005-03|Efficient computer interfaces using continuous gestures, language models, and speech|Keith Vertanen |46|mphil-cstit=Darwin College,2004-07 628|2005-03|A formal security policy for an NHS electronic health record service|Moritz Y. Becker |81| 629|2005-04|Hybrid routing: A pragmatic approach to mitigating position uncertainty in geo-routing|Meng How Lim , Adam Greenhalgh, Julian Chesterfield , Jon Crowcroft |26| 630|2005-04|Semi-invasive attacks – A new approach to hardware security analysis|Sergei P. Skorobogatov |144|phd=Darwin College,2004-09 631|2005-04|MIRRORS: An integrated framework for capturing real world behaviour for models of ad hoc networks|Wenjun Hu , Jon Crowcroft |16| 632|2005-04|Between shallow and deep: an experiment in automatic summarising|R.I. Tucker , K. Spärck Jones |34| 633|2005-05|On deadlock, livelock, and forward progress|Alex Ho , Steven Smith , Steven Hand |8| 634|2005-05|Visualisation, interpretation and use of location-aware interfaces|Kasim Rehman |159|phd=St Catharine’s College,2004-11 635|2005-06|Results from 200 billion iris cross-comparisons|John Daugman |8| 636|2005-07|Mind-reading machines: automated inference of complex mental states|Rana Ayman el Kaliouby |185|phd=Newnham College,2005-03 637|2005-07|The topology of covert conflict|Shishir Nagaraja , Ross Anderson |15| 638|2005-07|Optimistic Generic Broadcast|Piotr Zieliński |22| 639|2005-09|Non-blocking hashtables with open addressing|Chris Purcell , Tim Harris |23| 640|2005-07|Combining cryptography with biometrics effectively|Feng Hao , Ross Anderson , John Daugman |17| 641|2005-08|Cryptographic processors – a survey|Ross Anderson , Mike Bond , Jolyon Clulow , Sergei Skorobogatov |19| 642|2005-08|First-class relationships in an object-oriented language|Gavin Bierman , Alisdair Wren |53| 643|2005-08|Using trust and risk for access control in Global Computing|Nathan E. Dimmock |145|phd=Jesus College,2005-04 644|2005-08|Robbing the bank with a theorem prover|Paul Youn, Ben Adida, Mike Bond , Jolyon Clulow , Jonathan Herzog, Amerson Lin, Ronald L. Rivest, Ross Anderson |26| 645|2005-08|RFID is X-ray vision|Frank Stajano |10| 646|2005-09|A survey of Wireless Sensor Network technologies: research trends and middleware’s role|Eiko Yoneki , Jean Bacon |46|deleted=2006-04,withdrawn by Eiko Yoneki due to “some major mistakes in it”, planned update never emerged 647|2005-10|An agent architecture for simulation of end-users in programming-like tasks|Sam Staton |12| 648|2005-10|Cassandra: flexible trust management and its application to electronic health records|Moritz Y. Becker |214|phd=Trinity College,2005-09 649|2005-10|The decolorize algorithm for contrast enhancing, color to grayscale conversion|Mark Grundland , Neil A. Dodgson |15|colour 650|2005-10|Parallel iterative solution method for large sparse linear equation systems|Rashid Mehmood , Jon Crowcroft |22| 651|2005-10|End-user programming in multiple languages|Rob Hague |122|phd=Fitzwilliam College,2004-07 652|2005-11|Discriminative training methods and their applications to handwriting recognition|Roongroj Nopsuwanchai |186|phd=Downing College,2004-08 653|2005-11|Anonymity and traceability in cyberspace|Richard Clayton |189|phd=Darwin College,2005-08 654|2005-11|Local reasoning for Java|Matthew J. Parkinson |120|phd=Churchill College,2005-08 655|2005-11|Wearing proper combinations|Karen Spärck Jones |27| 656|2005-11|Seamless mobility in 4G systems|Pablo Vidales |141|phd=Girton College,2005-05 657|2006-01|Security protocol design by composition|Hyun-Jin Choi |155|phd=Churchill College,2004-12 658|2006-01|Intrinsic point-based surface processing|Carsten Moenning |166|phd=Queens’ College,2005-01 659|2006-01|A safety proof of a lazy concurrent list-based set implementation|Viktor Vafeiadis , Maurice Herlihy, Tony Hoare , Marc Shapiro|19| 660|2006-02|Static program analysis based on virtual register renaming|Jeremy Singer |183|phd=Christ’s College,2005-03 661|2006-03|Compatible RMRS representations from RASP and the ERG|Anna Ritchie |41| 662|2006-03|An introduction to tag sequence grammars and the RASP system parser|Ted Briscoe |30| 663|2006-03|Syntax-driven analysis of context-free languages with respect to fuzzy relational semantics|Richard Bergmair |49| 664|2006-04|Designing knowledge: An interdisciplinary experiment in research infrastructure for shared description|Alan F. Blackwell |18| 665|2006-04|Security evaluation at design time for cryptographic hardware|Huiyun Li |81|phd=Trinity Hall,2005-12 666|2006-06|A pact with the Devil|Mike Bond , George Danezis |14| 667|2006-06|Minimizing latency of agreement protocols|Piotr Zieliński |239|phd=Trinity Hall,2005-09 668|2006-06|Optimistically Terminating Consensus|Piotr Zieliński |35| 669|2006-06|Active privilege management for distributed access control systems|David M. Eyers |222|phd=King’s College,2005-06 670|2006-07|On the application of program analysis and transformation to high reliability hardware|Sarah Thompson |215|phd=St Edmund’s College,2006-04 671|2006-07|Low-latency Atomic Broadcast in the presence of contention|Piotr Zieliński |23| 672|2006-08|Decomposing file data into discernible items|Calicrates Policroniades-Borraz |230|phd=Hughes Hall,2005-12 673|2006-08|Probabilistic word sense disambiguation\\Analysis and techniques for combining knowledge sources|Judita Preiss |108|phd=Trinity College,2005-07 674|2006-10|Landmark Guided Forwarding|Meng How Lim |109|phd=St Catharine’s College,2006-09 675|2006-11|Computational models for first language acquisition|Paula J. Buttery |176|phd=Churchill College,2006-03 676|2006-12|Road traffic analysis using MIDAS data: journey time prediction|R.J. Gibbens , Y. Saacti|35|front=Department for Transport Horizons Research Programme “Investigating the handling of large transport related datasets” (project number H05-217) 677|2006-12|ECCO: Data centric asynchronous communication|Eiko Yoneki |210|phd=Lucy Cavendish College,2006-09 678|2006-12|Compact forbidden-set routing|Andrew D. Twigg |115|phd=King’s College,2006-06 679|2007-01|Automatic summarising: a review and discussion of the state of the art|Karen Spärck Jones |67| 680|2007-01|Haggle: Clean-slate networking for mobile devices|Jing Su, James Scott , Pan Hui , Eben Upton , Meng How Lim , Christophe Diot, Jon Crowcroft , Ashvin Goel, Eyal de Lara|30| 681|2007-04|Indirect channels: a bandwidth-saving technique for fault-tolerant protocols|Piotr Zieliński |24| 682|2007-04|Translating HOL functions to hardware|Juliano Iyoda |89|phd=Hughes Hall,2006-10 683|2007-04|Simulation of colliding constrained rigid bodies|Martin Kleppmann |65|back=This technical report is based on a final-year project dissertation for the Computer Science Tripos. It was submitted in May 2006. The dissertation was marked as the best dissertation in its year and was awarded the AT&T prize. 684|2007-05|Bubble Rap: Forwarding in small world DTNs in ever decreasing circles|Pan Hui , Jon Crowcroft |44| 685|2007-05|Effect of severe image compression on iris recognition performance|John Daugman , Cathryn Downing |20| 686|2007-05|Dependable systems for Sentient Computing|Andrew C. Rice |150|php=Churchill College,2006-09 687|2007-06|A marriage of rely/guarantee and separation logic|Viktor Vafeiadis , Matthew Parkinson |31| 688|2007-06|Name-passing process calculi: operational models and structural operational semantics|Sam Staton |245|phd=Girton College,2006-12|updated=2008-03 689|2007-06|Removing polar rendering artifacts in subdivision surfaces|Ursula H. Augsdörfer, Neil A. Dodgson , Malcolm A. Sabin |7| 690|2007-06|Cluster storage for commodity computation|Russell Glen Ross |178|phd=Wolfson College,2006-12 691|2007-08|Preconditions on geometrically sensitive subdivision schemes|Neil A. Dodgson , Malcolm A. Sabin , Richard Southern |13| 692|2007-07|Toward an undergraduate programme in Interdisciplinary Design|Alan F. Blackwell |13| 693|2007-07|Automatic classification of eventual failure detectors|Piotr Zieliński |21| 694|2007-07|Anti-Ω: the weakest failure detector for set agreement|Piotr Zieliński |24| 695|2007-07|Efficient maximum-likelihood decoding of spherical lattice codes|Karen Su , Inaki Berenguer , Ian J. Wassell , Xiaodong Wang|29| 696|2007-08|An introduction to inertial navigation|Oliver J. Woodman |37| 697|2007-08|Scaling Mount Concurrency: scalability and progress in concurrent algorithms|Chris J. Purcell |155|phd=Trinity College,2007-07 698|2007-09|Pulse-based, on-chip interconnect|Simon J. Hollis |186|phd=Queens’ College,2007-06 699|2007-10|A smooth manifold based construction of approximating lofted surfaces|Richard Southern , Neil A. Dodgson |17| 700|2007-10|Context aware service composition|Maja Vuković |225|phd=Newnham College,2006-04 701|2007-10|Vector microprocessors for cryptography|Jacques Jean-Alain Fournier |174|phd=Trinity Hall,2007-04 702|2007-11|Relationships for object-oriented programming languages|Alisdair Wren |153|phd=Sidney Sussex College,2007-03 703|2007-11|Lazy Susan: dumb waiting as proof of work|Jon Crowcroft , Tim Deegan , Christian Kreibich , Richard Mortier , Nicholas Weaver|23| 704|2007-11|Complexity and infinite games on finite graphs|Paul William Hunter |170|phd=Hughes Hall,2007-07 705|2007-12|Optimizing compilation with the Value State Dependence Graph|Alan C. Lawrence |183|phd=Churchill College,2007-05|colour 706|2007-12|Covert channel vulnerabilities in anonymity systems|Steven J. Murdoch |140|phd=Girton College,2007-08 707|2007-12|Complexity-effective superscalar embedded processors using instruction-level distributed processing|Ian Caulfield |130|phd=Queens’ College,2007-05 708|2008-01|IDRM: Inter-Domain Routing Protocol for Mobile Ad Hoc Networks|Chi-Kin Chau , Jon Crowcroft , Kang-Won Lee, Starsky H.Y. Wong|24| 709|2008-01|Protocols and technologies for security in pervasive computing and communications|Ford Long Wong |167|phd=Girton College,2007-08 710|2008-02|Event structures with persistence|Lucy G. Brace-Evans |113|phd=St. John’s College,2007-10 711|2008-02|Thinking inside the box: system-level failures of tamper proofing|Saar Drimer , Steven J. Murdoch , Ross Anderson |37| 712|2008-03|Flash-exposure high dynamic range imaging: virtual photography and depth-compensating flash|Christian Richardt |9| 713|2008-03|People are the network: experimental design and evaluation of social-based forwarding algorithms|Pan Hui |160|phd=Churchill College,2007-07 714|2008-03|A wide-area file system for migrating virtual machines|Tim Moreton |163|phd=King’s College,2007-02 715|2008-04|On using fuzzy data in security mechanisms|Feng Hao |69|phd=Queens’ College,2007-04 716|2008-04|UpgradeJ: Incremental typechecking for class upgrades|Gavin M. Bierman , Matthew J. Parkinson , James Noble|35| 717|2008-06|Psychologically-based simulation of human behaviour|Stephen Julian Rymill |250|phd=Jesus College,2006 718|2008-06|Cooperative attack and defense in distributed networks|Tyler Moore |172|phd=St. John’s College,2008-03 719|2008-06|The Intelligent Book: technologies for intelligent and adaptive textbooks, focussing on Discrete Mathematics|William H. Billingsley |156|phd=Wolfson College,2007-04 720|2008-06|A capability-based access control architecture for multi-domain publish/subscribe systems|Lauri I.W. Pesonen |175|phd=Wolfson College,2007-12 721|2008-06|Investigating classification for natural language processing tasks|Ben W. Medlock |138|phd=Fitzwilliam College,2007-09 722|2008-07|Energy-efficient sentient computing|Mbou Eyole-Monono |138|phd=Trinity College,2008-01 723|2008-07|Animation manifolds for representing topological alteration|Richard Southern |131|phd=Clare Hall,2008-02 724|2008-07|Bayesian inference for latent variable models|Ulrich Paquet |137|phd=Wolfson College,2007-03 725|2008-07|Beyond node degree: evaluating AS topology models|Hamed Haddadi , Damien Fay , Almerima Jamakovic, Olaf Maennel, Andrew W. Moore , Richard Mortier , Miguel Rio, Steve Uhlig|16| 726|2008-07|Modular fine-grained concurrency verification|Viktor Vafeiadis |148|phd=Selwyn College,2007-07 727|2008-09|A novel auto-calibration system for wireless sensor motes|Ruoshui Liu , Ian J. Wassell |65| 728|1997-02|A robust efficient algorithm for point location in triangulations|Peter J.C. Brown , Christopher T. Faigle |16|back=This report was written in February 1997 but not formally submitted to the Technical Report series until September 2008. 729|2008-09|Weighted spectral distribution|Damien Fay , Hamed Haddadi , Steve Uhlig, Andrew W. Moore , Richard Mortier , Almerima Jamakovic|13| 730|2008-08|Adaptive evaluation of non-strict programs|Robert J. Ennals |243|phd=King’s College,2004-06 731|2008-09|A new approach to Internet banking|Matthew Johnson |113|phd=Trinity Hall,2008-07 732|2008-11|Computing surfaces – a platform for scalable interactive displays|Alban Rrustemi |156|phd=St Edmund’s College,2008-11 733|2008-12|Tangible user interfaces for peripheral interaction|Darren Edge |237|phd=Jesus College,2008-01 734|2008-12|Tabletop interfaces for remote collaboration|Philip Tuddenham |243|phd=Gonville and Caius College,2008-06 735|2008-12|Learning compound noun semantics|Diarmuid Ó Séaghdha |167|phd=Corpus Christi College,2008-07 736|2009-01|Deny-guarantee reasoning|Mike Dodds , Xinyu Feng, Matthew Parkinson , Viktor Vafeiadis |82| 737|2008-12|Static contract checking for Haskell|Na Xu |175|phd=Churchill College,2008-08 738|2009-01|High precision timing using self-timed circuits|Scott Fairbanks |99|phd=Gonville and Caius College,2004-09|back=The PDF file provided by the author has minor font problems. 739|2009-01|State-based Publish/Subscribe for sensor systems|Salman Taherian |240|phd=St John’s College,2008-06 740|2009-01|Analysis of affective expression in speech|Tal Sobol-Shikler |163|phd=Girton College,2007-03|back=Many of the features and techniques presented in this report are subject to patent applications. 741|2009-01|Vehicular wireless communication|David N. Cottingham |264|phd=Churchill College,2008-09 742|2009-02|TCP, UDP, and Sockets:\\Volume 3: The Service-level Specification|Thomas Ridge, Michael Norrish , Peter Sewell |305| 743|2009-03|Optimising the speed and accuracy of a Statistical GLR Parser|Rebecca F. Watson |145|phd=Darwin College,2007-09 744|2009-03|Citation context analysis for information retrieval|Anna Ritchie |119|phd=New Hall,2008-06 745|2009-03|A better x86 memory model: x86-TSO\\(extended version)|Scott Owens , Susmit Sarkar , Peter Sewell |52| 746|2009-03|The snooping dragon: social-malware surveillance of the Tibetan movement|Shishir Nagaraja , Ross Anderson |12| 747|2009-03|An estimator of forward and backward delay for multipath transport|Fei Song , Hongke Zhang, Sidong Zhang, Fernando Ramos , Jon Crowcroft |16| 748|2009-04|GTVS: boosting the collection of application traffic ground truth|Marco Canini , Wei Li , Andrew W. Moore |20| 749|2009-05|Identifying social communities in complex communications for network efficiency|Pan Hui , Eiko Yoneki , Jon Crowcroft , Shu-Yan Chan |14| 750|2009-05|AtoZ: an automatic traffic organizer using NetFPGA|Marco Canini , Wei Li , Martin Zadnik , Andrew W. Moore |27| 751|2009-07|Nominal domain theory for concurrency|David C. Turner |185|phd=Clare College,2008-12 752|2009-07|Security of proximity identification systems|Gerhard P. Hancke |161|phd=Wolfson College,2008-02 753|2009-08|Carbon: trusted auditing for P2P distributed virtual environments|John L. Miller , Jon Crowcroft |20| 754|2009-08|Understanding scam victims: seven principles for systems security|Frank Stajano , Paul Wilson|22|front=An updated, abridged and peer-reviewed version of this report appeared in Communications of the ACM 54(3):70-75, March 2011 [doi:10.1145/1897852.1897872]. Please cite the refereed CACM version in any related work. 755|2009-09|Skin-detached surface for interactive large mesh editing|Yujian Gao , Aimin Hao, Qinping Zhao, Neil A. Dodgson |18| 756|2009-09|Analysis of the Internet’s structural evolution|Hamed Haddadi , Damien Fay , Steve Uhlig, Andrew W. Moore , Richard Mortier , Almerima Jamakovic|13| 757|2009-07|Improving cache performance by runtime data movement|Mark Adcock |174|phd=Christ’s College,2009-06|colour 758|2009-10|Logics and analyses for concurrent heap-manipulating programs|Alexey Gotsman |160|phd=Churchill College,2009-09 759|2011-08|Coarse-grained transactions\\(extended version)|Eric Koskinen , Matthew Parkinson , Maurice Herlihy|34| 760|2009-11|Radical innovation: crossing knowledge boundaries with interdisciplinary teams|Alan F. Blackwell , Lee Wilson, Alice Street, Charles Boulton, John Knell|124| 761|2009-11|Programming networks of vehicles|Jonathan J. Davies |292|phd=Churchill College,2008-09 762|2009-11|Resource provisioning for virtualized server applications|Evangelia Kalyvianaki |161|phd=Lucy Cavendish College,2008-08 763|2009-11|Security for volatile FPGAs|Saar Drimer |169|phd=Darwin College,2009-08 764|2009-12|Statistical anaphora resolution in biomedical texts|Caroline V. Gasperin |124|phd=Clare Hall,2008-08 765|2009-12|Formal verification of machine-code programs|Magnus O. Myreen |109|phd=Trinity College,2008-12 766|2009-12|Towards robust inexact geometric computation|Julian M. Smith |186|phd=St. Edmund’s College,2009-07|colour 767|2010-01|Ising model of rumour spreading in interacting communities|Massimo Ostilli, Eiko Yoneki , Ian X. Y. Leung , Jose F. F. Mendes, Pietro Lió, Jon Crowcroft |24| 768|2010-02|Report on existing open-source electronic medical records|Cecily Morrison , Adona Iosif , Miklos Danka|12|colour 769|2010-02|Kilim: A server framework with lightweight actors, isolation types and zero-copy messaging|Sriram Srinivasan |127|phd=King’s College,2010-02 770|2010-02|Controlling the dissemination and disclosure of healthcare events|Jatinder Singh |193|phd=St. John’s College,2009-09 771|2010-03|Bodies-in-Space: investigating technology usage in co-present group interaction|Cecily Morrison |147|phd=Darwin College,2009-08 772|2010-03|An executable meta-language for inductive definitions with binders|Matthew R. Lakin |171|phd=Queens’ College,2010-03 773|2010-03|NURBS-compatible subdivision surfaces|Thomas J. Cashman |99|phd=Queens’ College,2010-01|colour 774|2010-03|Explicit stabilisation for modular rely-guarantee reasoning|John Wickerson , Mike Dodds , Matthew Parkinson |29| 775|2010-03|Creating high-performance, statically type-safe network applications|Anil Madhavapeddy |169|phd=Robinson College,2006-04 776|2010-03|System tests from unit tests|Kathryn E. Gray , Alan Mycroft |27| 777|2010-04|Concurrent Abstract Predicates|Thomas Dinsdale-Young, Mike Dodds , Philippa Gardner , Matthew Parkinson , Viktor Vafeiadis |43| 778|2016-09|Automatically proving linearizability|Viktor Vafeiadis |19| 779|2010-04|A text representation language for contextual and distributional processing|Eric K. Henderson |207|phd=Fitzwilliam College,2009 780|2010-05|Cryptography and evidence|Michael Roe |75|phd=Clare College,1997-04 781|2010-06|Stage scheduling for CPU-intensive servers|Minor E. Gordon |119|phd=Jesus College,2009-12 782|2010-06|Petri net semantics|Jonathan M. Hayman |252|phd=Darwin College,2009-01 783|2010-07|Distributed complex event detection for pervasive computing|Dan O’Keeffe |170|phd=St. John’s College,2009-12 784|2010-07|Characterizing 10 Gbps network interface energy consumption|Ripduman Sohan , Andrew Rice , Andrew W. Moore , Kieran Mansley |10| 785|2010-07|Anonymity, information, and machine-assisted proof|Aaron R. Coble |171|phd=King’s College,2010-01 786|2010-08|Communication flows in power-efficient Networks-on-Chips|Arnab Banerjee |107|phd=Girton College,2009-03 787|2010-10|Emotion inference from human body motion|Daniel Bernhardt |227|phd=Selwyn College,2010-01 788|2011-07|Branching-time reasoning for programs\\(extended version)|Byron Cook, Eric Koskinen , Moshe Vardi|38| 789|2010-11|Making prophecies with decision predicates|Byron Cook, Eric Koskinen |29| 790|2010-11|Automated assessment of ESOL free text examinations|Ted Briscoe , Ben Medlock , Øistein Andersen |31| 791|2010-11|Semi-supervised learning for biomedical information extraction|Andreas Vlachos |113|phd=Peterhouse College,2009-12 792|2010-11|Machine learning and automated theorem proving|James P. Bridge |180|phd=Corpus Christi College,2010-10 793|2010-12|Affect inference in learning environments: a functional view of facial affect analysis using naturalistic data|Shazia Afzal |146|phd=Murray Edwards College,2010-05 794|2011-01|Grammatical error prediction|Øistein E. Andersen |163|phd=Girton College,2010 795|2011-02|Underspecified quantification|Aurelie Herbelot |163|phd=Trinity Hall,2010 796|2011-03|Facilitating program parallelisation: a profiling-based approach|Jonathan Mak |120|phd=St. John’s College,2010-11 797|2011-04|Interpretational overhead in system software|Boris Feigin |116|phd=Homerton College,2010-09 798|2011-06|Practical memory safety for C|Periklis Akritidis |136|phd=Wolfson College,2010-05 799|2011-06|A separation logic framework for HOL|Thomas Tuerk |271|phd=Downing College,2010-12 800|2011-06|Improving cache utilisation|James R. Srinivasan |184|phd=Jesus College,2011-04 801|2011-07|Software lock elision for x86 machine code|Amitabha Roy |154|phd=Emmanuel College,2011-04 802|2011-07|Latent semantic sentence clustering for multi-document summarization|Johanna Geiß |156|phd=St. Edmund’s College,2011-04 803|2011-08|Computational approaches to figurative language|Ekaterina V. Shutova |219|phd=Pembroke College,2011-03 804|2011-09|The HasGP user manual|Sean B. Holden |18| 805|2011-09|A model personal energy meter|Simon Hay |207|phd=Girton College,2011-08 806|2011-10|On joint diagonalisation for dynamic network analysis|Damien Fay , Jérôme Kunegis , Eiko Yoneki |12| 807|2011-10|Second-order algebraic theories|Ola Mahmoud |133|phd=Clare Hall,2011-03 808|2012-01|Resource-sensitive synchronisation inference by abduction|Matko Botinčan , Mike Dodds , Suresh Jagannathan |57| 809|2011-10|Distributed virtual environment scalability and security|John L. Miller |98|phd=Hughes Hall,2011-10 810|2011-11|Proximity Coherence for chip-multiprocessors|Nick Barrow-Williams |164|phd=Trinity Hall,2011-01 811|2011-12|Active electromagnetic attacks on secure hardware|A. Theodore Markettos |217|phd=Clare Hall,2010-03|colour 812|2012-01|Abstracting information on body area networks|Pedro Brandão |144|phd=Magdalene College,2011-07 813|2012-02|Reconstructing compressed photo and video data|Andrew B. Lewis |148|phd=Trinity College,2011-06|colour 814|2012-02|The free Internet: a distant mirage or near reality?|Arjuna Sathiaseelan , Jon Crowcroft |10| 815|2012-03|Colour videos with depth: acquisition, processing and evaluation|Christian Richardt |132|phd=Gonville & Caius College,2011-11|colour 816|2012-03|Verification of security protocols based on multicast communication|Jean E. Martina |150|phd=Clare College,2011-02 817|2012-03|The quest to replace passwords: a framework for comparative evaluation of Web authentication schemes|Joseph Bonneau , Cormac Herley, Paul C. van Oorschot, Frank Stajano |32| 818|2012-04|New approaches to operating system security extensibility|Robert N. M. Watson |184|phd=Wolfson College,2010-10 819|2012-05|Guessing human-chosen secrets|Joseph Bonneau |161|phd=Churchill College,2012-05 820|2012-08|A unified graph query layer for multiple databases|Eiko Yoneki , Amitabha Roy |22| 821|2012-10|Modelling energy efficiency for computation|Charles Reams |135|phd=Clare College,2012-10 822|2012-10|Planning with preferences using maximum satisfiability|Richard A. Russell |160|phd=Gonville and Caius College,2011-09 823|2012-11|Mitigating I/O latency in SSD-based graph traversal|Amitabha Roy , Karthik Nilakant , Valentin Dalibard , Eiko Yoneki |27| 824|2012-11|Hardware synthesis from a stream-processing functional language|Simon Frankau |202|phd=St. John’s College,2004-07 825|2012-12|Privacy engineering for social networks|Jonathan Anderson |255|phd=Trinity College,2012-07 826|2012-12|GREEN IPTV: a resource and energy efficient network for IPTV|Fernando M. V. Ramos |152|phd=Clare Hall,2012-11 827|2012-12|The smart card detective: a hand-held EMV interceptor|Omar S. Choudary |55|back=This technical report is based on a dissertation submitted by the author for the degree of Master of Philosophy (Advanced Computer Science) to the University of Cambridge, Darwin College. 828|2013-01|Exploring networks-on-chip for FPGAs|Rosemary M. Francis |121|phd=Darwin College,2009-07 829|2013-02|Microelectronic security measures|Philip Christopher Paul |177|phd=Pembroke College,2009-01|colour 830|2013-03|Massively parallel neural computation|Paul J. Fox |105|phd=Jesus College,2012-10 831|2013-04|Communication for programmability and performance on multi-core processors|Meredydd Luff |89|phd=Gonville & Caius College,2012-11 832|2013-04|Communication centric, multi-core, fine-grained processor architecture|Gregory A. Chadwick |165|phd=Fitzwilliam College,2012-09 833|2013-05|Practice-led design and evaluation of a live visual constraint language|Alan F. Blackwell , Ignatios Charalampidis|16| 834|2013-05|Concurrent verification for sequential programs|John Wickerson |149|phd=Churchill College,2012-12 835|2013-05|Call-by-need supercompilation|Maximilian C. Bolingbroke |230|phd=Robinson College,2013-04 836|2013-06|Aliasing contracts: a dynamic approach to alias protection|Janina Voigt , Alan Mycroft |27| 837|2013-06|Human-data interaction|Hamed Haddadi , Richard Mortier , Derek McAuley , Jon Crowcroft |9| 838|2013-06|Mining and tracking in evolving software|Silvia Breu |104|phd=Newnham College,2011-04 839|2013-09|Automatic extraction of property norm-like data from large text corpora|Colin Kelly |154|phd=Trinity Hall,2012-09 840|2013-09|Minimally supervised dependency-based methods for natural language processing|Marek Rei |169|phd=Churchill College,2012-12 841|2013-09|Information centric delay tolerant networking: an internet architecture for the challenged|Arjuna Sathiaseelan , Dirk Trossen , Ioannis Komnios, Joerg Ott , Jon Crowcroft |11| 842|2013-10|Automated assessment of English-learner writing|Helen Yannakoudakis |151|phd=Wolfson College,2012-12 843|2013-11|Programming for humans: a new paradigm for domain-specific languages|Robin Message |140|phd=Robinson College,2013-03 844|2013-11|Decompilation as search|Wei Ming Khoo |119|phd=Hughes Hall,2013-08 845|2013-12|Black-box composition of mismatched software components|Stephen Kell |251|phd=Christ’s College,2010-12 846|2014-01|Exploiting tightly-coupled cores|Daniel Bates |162|phd=Robinson College,2013-07 847|2014-02|SBUS: a generic policy-enforcing middleware for open pervasive systems|Jatinder Singh , Jean Bacon |20| 848|2014-02|Automatically generating reading lists|James G. Jardine |164|phd=Robinson College,2013-08 849|2014-03|SNA: Sourceless Network Architecture|Marcelo Bagnulo Braun, Jon Crowcroft |12| 850|2014-04|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-set architecture|Robert N.M. Watson , Peter G. Neumann , Jonathan Woodruff , Jonathan Anderson , David Chisnall , Brooks Davis , Ben Laurie , Simon W. Moore , Steven J. Murdoch , Michael Roe |131|back=Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the Department of Defense. Portions of this work were sponsored by the RCUK’s Horizon Digital Economy Research Hub grant, EP/G065802/1. Portions of this work were sponsored by Google, Inc. 851|2014-04|Capability Hardware Enhanced RISC Instructions: CHERI User’s guide|Robert N.M. Watson , David Chisnall , Brooks Davis , Wojciech Koszek , Simon W. Moore , Steven J. Murdoch , Peter G. Neumann , Jonathan Woodruff |26|back=Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the Department of Defense. 852|2014-04|Bluespec Extensible RISC Implementation: BERI Hardware reference|Robert N.M. Watson , Jonathan Woodruff , David Chisnall , Brooks Davis , Wojciech Koszek , A. Theodore Markettos , Simon W. Moore , Steven J. Murdoch , Peter G. Neumann , Robert Norton , Michael Roe |76|back=Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the Department of Defense. 853|2014-04|Bluespec Extensible RISC Implementation: BERI Software reference|Robert N.M. Watson , David Chisnall , Brooks Davis , Wojciech Koszek , Simon W. Moore , Steven J. Murdoch , Peter G. Neumann , Jonathan Woodruff |34|back=Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Defense Advanced Research Projects Agency or the Department of Defense. 854|2014-05|Programming contextual computations|Dominic Orchard |223|phd=Jesus College,2013-01 855|2014-06|Mephistophone|Patrick K.A. Wollner , Isak Herman , Haikal Pribadi, Leonardo Impett , Alan F. Blackwell |8| 856|2014-06|Sentiment analysis of scientific citations|Awais Athar |114|phd=Girton College,2014-04|colour 857|2014-07|ARC: Analysis of Raft Consensus|Heidi Howard |69|cst-part2=Pembroke College,2014-05 858|2014-07|CHERI: A RISC capability machine for practical memory safety|Jonathan D. Woodruff |112|phd=Clare Hall,2014-03 859|2014-09|Resourceful: fine-grained resource accounting for explaining service variability|Lucian Carata , Oliver Chick , James Snee , Ripduman Sohan , Andrew Rice , Andy Hopper |12| 860|2014-10|Program equivalence in functional metaprogramming via nominal Scott domains|Steffen Loesch |164|phd=Trinity College,2014-05 861|2014-10|Automatic facial expression analysis|Tadas Baltrusaitis |218|phd=Fitzwilliam College,2014-03|colour 862|2014-10|Surface modelling for 2D imagery|Henrik Lieng |177|phd=Fitzwilliam College,2014-06|colour 863|2014-11|Regional clouds: technical considerations|Jatinder Singh , Jean Bacon , Jon Crowcroft , Anil Madhavapeddy , Thomas Pasquier , W. Kuan Hon, Christopher Millard|18| 864|2014-12|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-set architecture|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Jonathan Anderson , David Chisnall , Brooks Davis , Ben Laurie , Simon W. Moore , Steven J. Murdoch , Michael Roe |142|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Portions of this work were sponsored by the RCUK’s Horizon Digital Economy Research Hub grant, EP/G065802/1. Portions of this work were sponsored by Google, Inc.|add-copyright-owner=SRI International 865|2014-12|I/O Optimisation and elimination via partial evaluation|Christopher S.F. Smowton |129|phd=Churchill College,2014-11 866|2015-04|PDTL: Parallel and distributed triangle listing for massive graphs|Ilias Giechaskiel , George Panagopoulos , Eiko Yoneki |14| 867|2015-04|Higher-order proof translation|Nikolai Sultana |158|phd=Trinity College,2014-04 868|2015-04|Bluespec Extensible RISC Implementation: BERI Hardware reference|Robert N. M. Watson , Jonathan Woodruff , David Chisnall , Brooks Davis , Wojciech Koszek , A. Theodore Markettos , Simon W. Moore , Steven J. Murdoch , Peter G. Neumann , Robert Norton , Michael Roe |82|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Portions of this work were sponsored by Google, Inc.|add-copyright-owner=SRI International 869|2015-04|Bluespec Extensible RISC Implementation: BERI Software reference|Robert N. M. Watson , David Chisnall , Brooks Davis , Wojciech Koszek , Simon W. Moore , Steven J. Murdoch , Peter G. Neumann , Jonathan Woodruff |27|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Portions of this work were sponsored by Google, Inc.|add-copyright-owner=SRI International 870|2015-05|Accelerating control-flow intensive code in spatial hardware|Ali Mustafa Zaidi |170|phd=St. Edmund’s College,2014-02 871|2015-07|Architecture-neutral parallelism via the Join Calculus|Peter R. Calvert |150|phd=Trinity College,2014-09 872|2015-07|The integration of higher order interactive proof with first order automatic theorem proving|Jia Meng |144|phd=Churchill College,2005-04 873|2015-08|Clean application compartmentalization with SOAAP (extended version)|Khilan Gudka , Robert N.M. Watson , Jonathan Anderson , David Chisnall , Brooks Davis , Ben Laurie , Ilias Marinos , Peter G. Neumann , Alex Richardson |35|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”), FA8750-11-C-0249 (“MRC2”) and FA8650-15-C-7758 (CADETS) as part of the DARPA CRASH, MRC and CADETS research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from the Google SOAAP Focused Research Award, the Isaac Newton Trust, the EPSRC REMS Programme Grant (EP/K008528/1), the NSERC Discovery Grant (RGPIN/06048-2015), and Thales E-Security.|add-copyright-owner=SRI International 874|2015-09|Augmented Reality interfaces for symbolic play in early childhood|Zhen Bai |292|phd=Jesus College,2014-09 875|2015-09|The language of collaborative tagging|Theodosia Togia |203|phd=Trinity Hall,2015-09|colour 876|2015-09|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Jonathan Anderson , David Chisnall , Brooks Davis , Alexandre Joannou , Ben Laurie , Simon W. Moore , Steven J. Murdoch , Robert Norton , Stacey Son|198|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and FA8750-11-C-0249 (“MRC2”) as part of the DARPA CRASH and DARPA MRC research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from St John’s College Cambridge, the SOAAP Google Focused Research Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), and Thales E-Security.|add-copyright-owner=SRI International 877|2015-09|Capability Hardware Enhanced RISC Instructions: CHERI Programmer’s Guide|Robert N. M. Watson , David Chisnall , Brooks Davis , Wojciech Koszek , Simon W. Moore , Steven J. Murdoch , Peter G. Neumann , Jonathan Woodruff |58|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) as part of the DARPA CRASH research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.|add-copyright-owner=SRI International 878|2015-09|Efficient multivariate statistical techniques for extracting secrets from electronic devices|Marios O. Choudary |164|phd=Darwin College,2014-07|isbn=978-0-901224-10-1 879|2016-02|Self-compilation and self-verification|Ramana Kumar |148|phd=Peterhouse College,2015-05 880|2016-02|Access contracts: a dynamic approach to object-oriented access protection|Janina Voigt |171|phd=Trinity College,2014-05 881|2016-03|Web data knowledge extraction|Juan M. Tirado, Ovidiu Serban , Qiang Guo , Eiko Yoneki |60|back=Acknowledgement: The research is funded by the H2020 DIGIWHIST project (645852) and is part-funded by the EPSRC DDEPI Project, EP/H003959. 882|2016-03|Discovering and exploiting parallelism in DOACROSS loops|Niall Murphy |129|phd=Darwin College,2015-09 883|2016-03|Survey propagation applied to weighted partial maximum satisfiability|Richard Russell , Sean B. Holden |15| 884|2016-04|Machine learning and computer algebra|Zongyan Huang |113|phd=Lucy Cavendish College,2015-08 885|2016-04|HasGP: A Haskell library for Gaussian process inference|Sean B. Holden |6| 886|2016-05|Error detection in content word combinations|Ekaterina Kochmar |170|phd=St. John’s College,2014-12 887|2016-05|Hardware support for compartmentalisation|Robert M. Norton |86|phd=Clare Hall,2015-09|back=With thanks to Microsoft Research Limited who provided the primary funding for this work via their PhD scholarship program under contract MRL-2011-031.\_Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and FA8750-11-C-0249 (“MRC2”) as part of the DARPA CRASH and DARPA MRC research programs. The views, opinions, and/or findings contained in this report are those of the author and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. 888|2016-05|Recomputation-based data reliability for MapReduce using lineage|Sherif Akoush , Ripduman Sohan , Andy Hopper |19| 889|2016-05|Evaluating the viability of remote renewable energy in datacentre computing|Sherif Akoush , Ripduman Sohan , Andrew Rice , Andy Hopper |26| 890|2016-06|Using multiple representations to develop notational expertise in programming|Alistair G. Stead |301|phd=Girton College,2015-05 891|2016-06|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 5)|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Jonathan Anderson , David Chisnall , Brooks Davis , Alexandre Joannou , Ben Laurie , Simon W. Moore , Steven J. Murdoch , Robert Norton , Stacey Son, Hongyan Xia |242|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and FA8750-11-C-0249 (“MRC2”) as part of the DARPA CRASH and DARPA MRC research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), and Thales E-Security.|add-copyright-owner=SRI International 892|2016-07|Pipelined image processing for pattern recognition|A. Daniel Hall |121|phd=Queen’s College,1991-10 893|2016-07|Towards practical information flow control and audit|Thomas F. J.-M. Pasquier |153|phd=Jesus College,2016-01 894|2016-09|Issues in preprocessing current datasets for grammatical error correction|Christopher Bryant , Mariano Felice |15| 895|2016-10|Artificial error generation for translation-based grammatical error correction|Mariano Felice |155|phd=Hughes Hall,2016-10|updated=2016-11 896|2016-12|Learning to de-anonymize social networks|Kumar Sharad |158|phd=Churchill College,2016-11 897|2017-01|Characterization of Internet censorship from multiple perspectives|Sheharbano Khattak |170|phd=Robinson College,2017-01 898|2017-01|Access control for network management|Dongting Yu |108|phd=Robinson College,2016-05 899|2017-02|Deep embodiment: grounding semantics in perceptual modalities|Douwe Kiela |128|phd=Darwin College,2016-07 900|2017-02|A framework to build bespoke auto-tuners with structured Bayesian optimisation|Valentin Dalibard |182|phd=St. John’s College,2017-01 901|2017-02|Signal maps for smartphone localisation|Chao Gao |127|phd=King’s College,2016-08 902|2017-02|Programming language evolution|Raoul-Gabriel Urma |129|phd=Hughes Hall,2015-09 903|2017-02|Parameterized complexity of distances to sparse graph classes|Jannis Bulian |133|phd=Clare College,2016-02 904|2017-03|Grammatical error correction in non-native English|Zheng Yuan |145|phd=St. Edmund’s College,2016-09 905|2017-03|Fixed point promotion: taking the induction out of automated induction|William Sonnex |170|phd=Trinity College,2015-09 906|2017-03|Context-aware programming languages|Tomas Petricek |218|phd=Clare Hall,2017-03 907|2017-04|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 6)|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Jonathan Anderson , John Baldwin , David Chisnall , Brooks Davis , Alexandre Joannou , Ben Laurie , Simon W. Moore , Steven J. Murdoch , Robert Norton , Stacey Son, Hongyan Xia |307|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and FA8750-11-C-0249 (“MRC2”) as part of the DARPA CRASH and DARPA MRC research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, ARM Ltd, and HP Enterprise.|add-copyright-owner=SRI International 908|2017-07|ASAP: As Static As Possible memory management|Raphaël L. Proust |147|phd=Magdalene College,2016-07 909|2017-07|Exploring new attack vectors for the exploitation of smartphones|Laurent Simon |167|phd=Homerton College,2016-04 910|2017-07|Automated verification of continuous and hybrid dynamical systems|William Denman |178|phd=Clare College,2014-09 911|2017-09|Proofs for ‘Verifying Spatial Properties of Array Computations’|Dominic Orchard , Mistral Contrastin , Matthew Danish , Andrew Rice |8| 912|2017-09|Network traffic classification via neural networks|Ang Kun Joo Michael , Emma Valla , Natinael Solomon Neggatu , Andrew W. Moore |25| 913|2017-10|Hierarchical statistical semantic translation and realization|Matic Horvat |215|phd=Churchill College,2017-03 914|2017-11|Characterizing the impact of network latency on cloud-based applications’ performance|Diana Andreea Popescu , Noa Zilberman , Andrew W. Moore |20|updated=2017-12 915|2017-12|Annotating errors and disfluencies in transcriptions of speech|Andrew Caines , Diane Nicholls, Paula Buttery |10| 916|2018-02|Capability Hardware Enhanced RISC Instructions (CHERI): Notes on the Meltdown and Spectre Attacks|Robert N. M. Watson , Jonathan Woodruff , Michael Roe , Simon W. Moore , Peter G. Neumann |16|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and FA8750-11-C-0249 (“MRC2”), as part of the DARPA CRASH and MRC research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, ARM Ltd, and HP Enterprise.|add-copyright-owner=SRI International 917|2018-03|Formal verification-driven parallelisation synthesis|Matko Botinčan |163|phd=Trinity College,2013-09 918|2018-03|Evaluation of decentralized email architecture and social network analysis based on email attachment sharing|Gregory Y. Tsipenyuk |153|phd=Sidney Sussex College,2017-08 919|2018-03|Proceedings of the 2017 Scheme and Functional Programming Workshop|Nada Amin , François-René Rideau|50|front=Oxford, UK – 3 September 2017 920|2018-05|Interactive analytical modelling|Advait Sarkar |142|phd=Emmanuel College,2016-12|colour 921|2018-06|Optimising data centre operation by removing the transport bottleneck|Toby Moncaster |130|phd=Wolfson College,2018-02 922|2018-06|Raising a new generation of cyber defenders|Frank Stajano , Graham Rymer , Michelle Houghton |307| 923|2018-07|Prefetching for complex memory access patterns|Sam Ainsworth |146|phd=Churchill College,2018-02 924|2018-08|OpenDTrace Specification version 1.0|George Neville-Neil , Jonathan Anderson , Graeme Jenkinson , Brian Kidney, Domagoj Stolfa , Arun Thomas , Robert N. M. Watson |235|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8650-15-C-7558 (“CADETS”) as part of the DARPA Transparent Computing research program. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. 925|2018-09|Privacy markets in the Apps and IoT age|Ranjan Pal , Jon Crowcroft , Abhishek Kumar , Pan Hui, Hamed Haddadi , Swades De, Irene Ng, Sasu Tarkoma, Richard Mortier |45| 926|2018-10|Are cyber-blackouts in service networks likely?: implications for cyber risk management|Ranjan Pal , Konstantinos Psounis, Abhishek Kumar , Jon Crowcroft , Pan Hui, Leana Golubchik, John Kelly, Aritra Chatterjee, Sasu Tarkoma|32| 927|2019-06|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7)|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Hesham Almatary , Jonathan Anderson , John Baldwin , David Chisnall , Brooks Davis , Nathaniel Wesley Filardo , Alexandre Joannou , Ben Laurie , A. Theodore Markettos , Simon W. Moore , Steven J. Murdoch , Kyndylan Nienhuis , Robert Norton , Alex Richardson , Peter Rugg , Peter Sewell , Stacey Son, Hongyan Xia |496|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”), FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), and FA8650-18-C-7809 (“CIFV”) as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, a Google Chrome University Research Program Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the EPSRC IOSEC grant (EP/EP/R012458/1), the ERC Advanced Grant ELVER (789108), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google DeepMind, HP Enterprise, and a Gates Cambridge Scholarship.|add-copyright-owner=SRI International 928|2018-11|Cut-through network switches: architecture, design and implementation|Noa Zilberman , Łukasz Dudziak, Matthew Jadczak, Thomas Parks, Alessandro Rietmann, Vadim Safronov, Daniel Zuo|18| 929|2018-11|Resilient payment systems|Khaled Baqer |115|phd=St. Edmund’s College,2018-10 930|2018-12|Provenance-based computing|Lucian Carata |132|phd=Wolfson College,2016-07 931|2019-01|A Performance-efficient and practical processor error recovery framework|Jyothish Soman |91|phd=Wolfson College,2017-07 932|2019-04|CheriABI: Enforcing valid pointer provenance and minimizing pointer privilege in the POSIX C run-time environment|Brooks Davis , Robert N. M. Watson , Alexander Richardson , Peter G. Neumann , Simon W. Moore , John Baldwin , David Chisnall , Jessica Clarke , Nathaniel Wesley Filardo , Khilan Gudka , Alexandre Joannou , Ben Laurie , A. Theodore Markettos , J. Edward Maste , Alfredo Mazzinghi , Edward Tomasz Napierala , Robert M. Norton , Michael Roe , Peter Sewell , Stacey Son, Jonathan Woodruff |40|back=This technical report extends our paper of the same title published at ASPLOS 2019 with a focus on implementation details of interest to operating system and compiler developers.\_Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and HR0011-18-C-0016 (“ECATS”), as part of the DARPA CRASH, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, a Google Chrome University Research Program Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the ERC Advanced Grant ELVER (789108), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google DeepMind, and HP Enterprise.|add-copyright-owner=SRI International|updated=2020-03 933|2019-01|An Evaluation of NDP performance|Noa Zilberman |19| 934|2019-02|Exploitation from malicious PCI Express peripherals|Colin L. Rothwell |108|pnd=Churchill College,2017-09 935|2019-04|Distributed consensus revised|Heidi Howard |151|phd=Pembroke College,2018-09 936|2019-05|High-performance memory safety: optimizing the CHERI capability machine|Alexandre J. P. Joannou |132|phd=Peterhouse College,2017-09 937|2019-06|Latency-driven performance in data centres|Diana Andreea Popescu |190|phd=Churchill College,2018-12 938|2019-06|Automatic annotation of error types for grammatical error correction|Christopher Bryant |138|phd=Churchill College,2018-12 939|2019-08|Effects of timing on users’ perceived control when interacting with intelligent systems|Christine Guo Yu |284|phd=Gonville & Caius Gollege,2018-05 940|2019-09|Rigorous engineering for hardware security: formal modelling and proof in the CHERI design and implementation process|Kyndylan Nienhuis , Alexandre Joannou , Anthony Fox, Michael Roe , Thomas Bauereiss , Brian Campbell, Matthew Naylor , Robert M. Norton , Simon W. Moore , Peter G. Neumann , Ian Stark , Robert N. M. Watson , Peter Sewell |38|back=This work was supported by EPSRC programme grant EP/K008528/1 (REMS: Rigorous Engineering for Mainstream Systems). This work was supported by a Gates studentship (Nienhuis). This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement 789108). This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (CTSRD), HR0011-18-C-0016 (ECATS), and FA8650-18-C-7809 (CIFV). The views, opinions, and/or findings contained in this paper are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. Approved for public release; distribution is unlimited.|add-copyright-owner=SRI International 941|2019-09|An Introduction to CHERI|Robert N. M. Watson , Simon W. Moore , Peter Sewell , Peter G. Neumann |43|back=Approved for public release; distribution is unlimited\_This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”), with additional support from FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), and FA8650-18-C-7809 (“CIFV”) as part of the DARPA CRASH, MRC, and SSITH research programs.\_The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.\_We also acknowledge the EPSRC REMS Programme Grant (EP/K008528/1), the ERC ELVER Advanced Grant (789108), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google, Google DeepMind, HP Enterprise, and the Gates Cambridge Trust.|add-copyright-owner=SRI International|updated=2019-10,2020-07 942|2020-01|Evaluating visually grounded language capabilities using microworlds|Alexander Kuhnle |142|phd=Queens’ College,2019-08 943|2020-01|Latency-First datacenter network scheduling|Mathew P. Grosvenor |310|phd=,2017-04 944|2020-02|Honeypots in the age of universal attacks and the Internet of Things|Alexander Vetterl |115|phd=Churchill College,2019-11 945|2020-03|Machine learning methods for detecting structure in metabolic flow networks|Maxwell Jay Conway |132|phd=Selwyn College,2018-08 946|2020-04|End-to-end deep reinforcement learning in computer systems|Michael Schaarschmidt |166|phd=Sidney Sussex College,2019-09 947|2020-06|CHERI C/C++ Programming Guide|Robert N. M. Watson , Alexander Richardson , Brooks Davis , John Baldwin , David Chisnall , Jessica Clarke , Nathaniel Filardo , Simon W. Moore , Edward Napierala , Peter Sewell , Peter G. Neumann |33|back=This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and HR0011-18-C-0016 (“ECATS”). The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. This work was supported in part by the Innovate UK project Digital Security by Design (DSbD) Technology Platform Prototype, 105694. This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 789108), ERC Advanced Grant ELVER. We also acknowledge the EPSRC REMS Programme Grant (EP/K008528/1), Arm Limited, HP Enterprise, and Google, Inc. Approved for Public Release, Distribution Unlimited.|add-copyright-owner=SRI International 948|2020-06|Reasoning about effectful programs and evaluation order|Dylan McDermott |150|phd=Homerton College,2019-10 949|2020-06|Complete spatial safety for C and C++ using CHERI capabilities|Alexander Richardson |189|phd=Emmanuel College,2019-10|back=This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”) and HR0011-18-C-0016 (“ECATS”) as part of the DARPA CRASH and SSITH research programs.\_The views, opinions, and/or findings contained in this report are those of the author and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.\_This work was supported in part by HP Enterprise, Arm Limited and Google, Inc.\_Approved for Public Release, Distribution Unlimited. 950|2020-08|Probabilistic concurrent game semantics|Hugo Paquet |156|phd=Homerton College,2019-09 951|2020-10|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8)|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Hesham Almatary , Jonathan Anderson , John Baldwin , Graeme Barnes , David Chisnall , Jessica Clarke , Brooks Davis , Lee Eisen, Nathaniel Wesley Filardo , Richard Grisenthwaite , Alexandre Joannou , Ben Laurie , A. Theodore Markettos , Simon W. Moore , Steven J. Murdoch , Kyndylan Nienhuis , Robert Norton , Alexander Richardson , Peter Rugg , Peter Sewell , Stacey Son, Hongyan Xia |590|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”), with additional support from FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), and FA8650-18-C-7809 (“CIFV”) as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.\_This work was supported in part by the Innovate UK project Digital Security by Design (DSbD) Technology Platform Prototype, 105694.\_Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, a Google Chrome University Research Program Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the EPSRC IOSEC grant (EP/EP/R012458/1), the ERC Advanced Grant ELVER (789108), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google DeepMind, HP Enterprise, and a Gates Cambridge Scholarship.|add-copyright-owner=SRI International 952|2020-10|Exploring the effect of spatial faithfulness on group decision-making|David Adeboye |64|mphil-acs=Jesus College,2020 953|2020-12|DSbD CHERI and Morello Capability Essential IP (Version 1)|Robert N. M. Watson , Jonathan Woodruff , Alexandre Joannou , Simon W. Moore , Peter Sewell , Arm Limited|25|back=This work was funded by the UK Government’s Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme delivered by UK Research and Innovation (UKRI), as part of the DSbD Technology Platform Prototype project (105694).\_Approved for public release; distribution is unlimited. Sponsored in part by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”), with additional support from FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), and FA8650-18-C-7809 (“CIFV”) as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.\_Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, a Google Chrome University Research Program Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the EPSRC IOSEC grant (EP/EP/R012458/1), the ERC Advanced Grant ELVER (789108), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google DeepMind, HP Enterprise, and a Gates Cambridge Scholarship. 954|2021-02|Inline and sideline approaches for low-cost memory safety in C|Myoung Jin Nam |124|phd=Selwyn College,2020-11 955|2021-02|Capability memory protection for embedded systems|Hongyan Xia |145|phd=Hughes Hall,2019-05 956|2021-04|Optimisation of a modern numerical library: a bottom-up approach|Jianxin Zhao |96|phd=Corpus Christi College,2019-09 957||Rollercoaster: an efficient group-multicast scheme for mix networks|Daniel Hugenroth , Martin Kleppmann , Alastair R. Beresford |27|front=Originally published in Proceedings of the 30th USENIX Security Symposium 958|2021-06|Machine-learning approaches for the empirical Schrödinger bridge problem|Francisco Vargas |114|mphil-acs=Girton College,2020-06-24|updated=2022-06 959|2021-09|Verified security for the Morello capability-enhanced prototype Arm architecture|Thomas Bauereiss , Brian Campbell , Thomas Sewell , Alasdair Armstrong , Lawrence Esswood , Ian Stark , Graeme Barnes , Robert N. M. Watson , Peter Sewell |24|back=This work was partially supported by the UK Government Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694), ERC AdG 789108 ELVER, EPSRC programme grant EP/K008528/1 REMS, Arm iCASE awards, EPSRC IAA KTF funding, the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google, Google DeepMind, HP Enterprise, and the Gates Cambridge Trust.\_Approved for public release; distribution is unlimited. This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts FA8750-10-C-0237 (“CTSRD”), FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), and FA8650-18-C-7809 (“CIFV”), as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. 960|2021-09|Data summarizations for scalable, robust and privacy-aware learning in high dimensions|Dionysis Manousakas |130|phd=Darwin College,2020-10 961|2021-09|CheriOS: designing an untrusted single-address-space capability operating system utilising capability hardware and a minimal hypervisor|Lawrence G. Esswood |195|phd=Churchill College,2020-07|back=Approved for public release; distribution is unlimited. Sponsored in part by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract HR0011-18-C-0016 (“ECATS”) as part of the DARPA SSITH research programs. The views, opinions, and/or findings contained in this report are those of the author and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government. This work was also supported by Arm Limited and an EPSRC ICASE award. 962|2021-10|Trusted reference monitors for Linux using Intel SGX enclaves|Harri Bell-Thomas |62|cst-part3=Jesus College,2020-06 963|2021-10|Capability-based access control for cyber physical systems|Michael G. Dodson |127|phd=Queens’ College,2021-07 964|2021-11|Information dissemination via random walks|Hayk Saribekyan |134|phd=St John’s College,2021-07 965|2021-11|Improving commercial LiFi network feasibility through rotation invariance, motion prediction, and bandwidth aggregation at the physical layer|Daniel M. Fisher , Jon A. Crowcroft |79|mphil-acs=Downing College,2020-05 966|2021-12|Obstacles to wearable computing|Helen Oliver |318|phd=Murray Edwards College,2020-06|front=Funded and supported by The Alan Turing Institute Doctoral Scheme 967|2022-01|Gaussian Pixie Autoencoder: Introducing Functional Distributional Semantics to continuous latent spaces|Primož Fabiani |50|mphil-acs=Hughes Hall,2021-06 968|2022-02|Evidence-based verification and correction of textual claims|James Thorne |231|phd=Peterhouse College,2021-09 969|2022-05|Assessing the understandability of a distributed algorithm by tweeting buggy pseudocode|Martin Kleppmann |15| 970|2022-05|Transparent analysis of multi-modal embeddings|Anita L. Verő |202|phd=King’s College,2021-11|colour 971|2022-06|Automating representation change across domains for reasoning|Aaron Stockdill |268|phd=Selwyn College,2021-09 972|2022-06|Muntjac multicore RV64 processor: introduction and microarchitectural guide|Xuan Guo , Daniel Bates , Robert Mullins , Alex Bradbury |27|back=This work was kindly supported by lowRISC CIC. 973|2022-07|Data-driven representations in brain science: modelling approaches in gene expression and neuroimaging domains|Tiago M. L. Azevedo |136|phd=Churchill College,2022-02-13|colour 974|2022-08|Dynamic analysis for concurrency optimisation|Indigo J. D. Orton |166|phd=Hughes Hall,2021-10 975|2022-11|Memory safety with CHERI capabilities: security analysis, language interpreters, and heap temporal safety|Brett Gutstein |119|phd=Trinity College,2022-07 976|2022-11|CHERI compartmentalisation for embedded systems|Hesham Almatary |142|phd=St John’s College,2022-02 977|2023-01|Motion quality models for real-time adaptive rendering|Akshay Jindal |132|phd=St Edmund’s College,2022-10|colour 978|2023-02|A Next Generation Internet Architecture|Alexander G. Fraser |118|contrib=edited::Elisabeth Fraser ;;foreword::Anil Madhavapeddy , David J. Scott |cc=by|copyright-year=2022 979|2023-02|Efficient virtual cache coherency for multicore systems and accelerators|Xuan Guo |202|phd=Peterhouse College,2022-09 980|2023-03|Protecting enclaves from side-channel attacks through physical isolation|Marno van der Maas |120|cc=by|phd=Clare Hall,2021-09 981|2023-05|The Cerberus C semantics|Kayvan Memarian |290|phd=Wolfson College,2022-10 982|2023-07|Arm Morello Programme: Architectural security goals and known limitations|Robert N. M. Watson , Graeme Barnes , Jessica Clarke , Richard Grisenthwaite , Peter Sewell , Simon W. Moore , Jonathan Woodruff |8|copyright-owner=Robert N. M. Watson, Jessica Clarke, Peter Sewell, Simon W. Moore, Jonathan Woodruff, Arm Limited|back=This work was supported by the Innovate UK project Digital Security by Design (DSbD) Technology Platform Prototype, 105694.\_We gratefully acknowledge UK Research and Innovation (UKRI), who sponsored the creation of Morello, and also the significant investment by DARPA in supporting the creation of CHERI and its earlier prototypes.\_We also acknowledge Arm Limited and Google, Inc. 983|2023-07|An evaluation of police interventions for cybercrime prevention|Maria Bada , Alice Hutchings , Yanna Papadodimitraki , Richard Clayton |80|back=Acknowledgements\_We would like to thank Prof Benoît Dupont and Prof David Wall for their useful comments and suggestions on this technical report. 984|2023-07|Efficient spatial and temporal safety for microcontrollers and application-class processors|Peter David Rugg |189|phd=Churchill College,2022-12 985|2023-08|Scalable agent-based models for optimized policy design: applications to the economics of biodiversity and carbon|Sharan S. Agrawal |84|mphil-acs=Darwin College,2023-06|cc=by 986|2023-09|Early performance results from the prototype Morello microarchitecture|Robert N. M. Watson , Jessica Clarke , Peter Sewell , Jonathan Woodruff , Simon W. Moore , Graeme Barnes , Richard Grisenthwaite , Kathryn Stacer, Silviu Baranga, Alexander Richardson |19|copyright-owner=Robert N. M. Watson, Jessica Clarke, Peter Sewell, Jonathan Woodruff, Simon W. Moore, Alexander Richardson, Arm Limited|back=This work was supported by Innovate UK project “Digital Security by Design (DSbD) Technology Platform Prototype”, 105694.\_Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) under contract HR0011-22-C-0110 (“ETC”). The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.\_We gratefully acknowledge UK Research and Innovation (UKRI), who sponsored the creation of Morello, and also the significant investment by DARPA in supporting the creation of CHERI and its earlier prototypes.\_We also acknowledge Arm Limited and Google, Inc. 987|2023-09|Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 9)|Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Hesham Almatary , Jonathan Anderson , John Baldwin , Graeme Barnes , David Chisnall , Jessica Clarke , Brooks Davis , Lee Eisen, Nathaniel Wesley Filardo , Franz A. Fuchs , Richard Grisenthwaite , Alexandre Joannou , Ben Laurie , A. Theodore Markettos , Simon W. Moore , Steven J. Murdoch , Kyndylan Nienhuis , Robert Norton , Alexander Richardson , Peter Rugg , Peter Sewell , Stacey Son, Hongyan Xia |523|back=Approved for public release; distribution is unlimited. Sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8750-10-C-0237 (“CTSRD”), with additional support from FA8750-11-C-0249 (“MRC2”), HR0011-18-C-0016 (“ECATS”), FA8650-18-C-7809 (“CIFV”), HR0011-22-C-0110 (“ETC”), and HR0011-23-C-0031 (“MTSS”) as part of the DARPA CRASH, MRC, and SSITH research programs. The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.\_This work was supported in part by the Innovate UK project Digital Security by Design (DSbD) Technology Platform Prototype, 105694.\_Additional support was received from St John’s College Cambridge, the Google SOAAP Focused Research Award, a Google Chrome University Research Program Award, the RCUK’s Horizon Digital Economy Research Hub Grant (EP/G065802/1), the EPSRC REMS Programme Grant (EP/K008528/1), the EPSRC Impact Acceleration Account (EP/K503757/1), the EPSRC IOSEC grant (EP/EP/R012458/1), the EPSRC CHaOS grant (EP/V000292/1), the EPSRC SIPP grant (EP/S030867/1), the ERC Advanced Grant ELVER (789108), the Isaac Newton Trust, the UK Higher Education Innovation Fund (HEIF), Thales E-Security, Microsoft Research Cambridge, Arm Limited, Google DeepMind, HP Enterprise, and a Gates Cambridge Scholarship.|add-copyright-owner=SRI International|cc=by 988|2023-10|CHERI C semantics as an extension of the ISO C17 standard|Vadim Zaliva , Kayvan Memarian , Ricardo Almeida , Jessica Clarke , Brooks Davis , Alex Richardson , David Chisnall , Brian Campbell , Ian Stark , Robert N. M. Watson , Peter Sewell |11|back=This work was supported by the UK Industrial Strategy Challenge Fund (ISCF) under the Digital Security by Design (DSbD) Programme, to deliver a DSbDtech enabled digital platform (grant 105694).\_This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 789108, ERC AdG ELVER).\_Distribution Statement A: Approved for public release; distribution is unlimited. This work was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contracts HR0011-22-C-0110 (“ETC”) and HR0011-23-C-0031 (“MTSS”). The views, opinions, and/or findings contained in this report are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.|add-copyright-owner=SRI International 989|2023-11|Balanced allocations under incomplete information: New settings and techniques|Dimitrios Los |230|phd=St John’s College,2023-04|cc=by 990|2023-12|Probing the foundations of neural algorithmic reasoning|Euan Ong |75|cst-part2=Trinity College,2023-05 991|2023-12|Porting a mix network client to mobile|Jacky W. E. Kung |57|cst-part2=St Edmund’s College,2023-05 992|2023-12|Transient execution vulnerabilities in the security context of server hardware|Allison Randal |145|phd=Robinson College,2023-07 #6??|2007-04|Virtual devices for virtual machines|Andrew K. Warfield |148|phd=Clare Hall,2006-05