# 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