Browse

ftp://theory.doc.ic.ac.uk (449)

	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/cill.ps.gz, 19911004 Computational Interpretations of Linear Logic Samson Abramsky Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate, London SW7 2BZ, England sa@doc.ic.ac.uk October 30, 1990
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/lazy.ps.gz, 19920123 The Lazy Lambda Calculus Samson Abramsky Department of Computing Imperial College of Science, Technology and Medicine Published in Research Topics in Functional Programming, ed. D. Turner, pages 65{117, Addison Wesley 1990 December 17, 1987 1 Introduction The commonly accepted basis for functional
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/gkp.ps.gz, 19920123 A Generalized Kahn Principle for Abstract Asynchronous Networks Samson Abramsky Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ England Published in the Proceedings of the Symposium on Mathematical Foundations of Programming Language
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/bisim.ps.gz, 19920123 A Domain Equation For Bisimulation Samson Abramsky Department of Computing Imperial College of Science, Technology and Medicine Published in Information and Computation 92,2 (1991), 161{218 January 2, 1990
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/dtlf.ps.gz, 19920123 Domain Theory In Logical Form Samson Abramsky Department of Computing Imperial College of Science and Technology 180 Queen's Gate London SW7 2BZ England Published in Annals of Pure and Applied Logic 51 (1991) 1{77 September 2, 1988
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/phd.ps.gz, 19920123 Domain Theory and the Logic of Observable Properties Samson Abramsky Submitted for the degree of Doctor of Philosophy Queen Mary College University of London October 5, 1987
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/cillfinalversion.ps.gz, 19920227 Computational Interpretations of Linear Logic Samson Abramsky Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate, London SW7 2BZ, England sa@doc.ic.ac.uk To appear in Theoretical Computer Science February 27, 1992
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/lics92.ps.gz, 19920401 New Foundations for the Geometry of Interaction Samson Abramsky Radha Jagadeesan Dept. of Computing Dept. of Computing Imperial College Imperial College London London. 1 Introduction A basic dichotomy runs through much of programming theory, assuming a number of guises: denotational/operational,
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/gfc.ps.gz, 19920925 Games and Full Completeness for Multiplicative Linear Logic Samson Abramsky and Radha Jagadeesan Department of Computing Imperial College of Science, Technology and Medicine Technical Report DoC 92/24 September 25, 1992
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/gfcsmallpage.ps.gz, 19920925 Games and Full Completeness for Multiplicative Linear Logic Samson Abramsky and Radha Jagadeesan Department of Computing Imperial College of Science, Technology and Medicine Technical Report DoC 92/24 September 25, 1992
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/nfgi.ps.gz, 19921210 New Foundations for the Geometry of Interaction Samson Abramsky Radha Jagadeesan Dept. of Computing Dept. of Computing Imperial College Imperial College London London. December 10, 1992 This research was supported by grants from UK SERC and ESPRIT Basic Research Action 3003 CLICS" 1 Contents 1
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/sdic.ps.gz, 19930514 Synchronous Dataflow in Interaction Categories Simon Gay Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7 2BZ, UK May 13, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Dawson/talks/internet/talk1.ps.gz, 19930616 What everyone should know about the Internet Mark Dawson Department of Computing What is the Internet The connected internet is a network of 8,258 networks con- taining 1,313,000 hosts reaching 13 million people. What can the Internet do for me The Internet is all about communicating information (for
	ftp://theory.doc.ic.ac.uk/theory/papers/Dawson/talks/internet/talk2.ps.gz, 19930617 Protocol Stacks A message passes from the sending process using a high- level protocol, through the Internet Layer, to the Network interface layer, across interveaning networks, and back upto the receiving process. Sender Receiver other... other... IP Layer Interface Net 1 Net 2 Net 3 IP Layer Interface
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/GeoTh+DBs.ps.gz, 19930624 pp. 288-314 in M.P. Fourman, P.T. Johnstone and A.M. Pitts (eds) Applications of Categories in Computer Science (Proceedings of the LMS Symposium, Durham 1991), London Mathematical Society Lecture Note Series 177, Cambridge University press 1992. Geometric Theories and Databases Steven Vickers *
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/PreFrPrePre.ps.gz, 19930624 pp. 193-212 in A. Carboni, M.C. Pedicchio and G. Rosolini (eds) Category Theory (Proceedings, Como 1990), Springer Lecture Notes in Mathematics 1488, 1991. PREFRAME PRESENTATIONS PRESENT Peter Johnstone, Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, 16 Mill Lane,
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/Infosys.ps.gz, 19930624 INFORMATION SYSTEMS FOR CONTINUOUS POSETS Steven Vickers, Department of Computing, Imperial College, 180 Queen s Gate, London, SW7 2BZ, England. email: sjv@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/GLiCS.ps.gz, 19930625 Geometric Logic in Computer Science Steve Vickers sjv@doc.ic.ac.uk Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/QuProc.ps.gz, 19930629 Math. Struct. in Computer Science (1993), vol. 3, pp. 161-227 QUANTALES, OBSERVATIONAL LOGIC AND PROCESS SEMANTICS Samson Abramsky Steven Vickers Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen s Gate, London, SW7 2BZ.
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.coquand.inf.ps.gz, 19930927 Infinite Objects in Type Theory Thierry Coquand Chalmers University Work in progress, Comments wellcome
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.kirch.BuB.ps.gz, 19930927 Bereiche und Bewertungen Olaf Kirch Juni 1993 Diplomarbeit am Fachbereich Mathematik der Technischen Hochschule Darmstadt Betreuender Professor: Prof. Klaus Keimel Inhaltsverzeichnis Liste der Symbole iii 1 Einfuhrung 1 1.1 Semantik von Programmiersprachen : : : : : : : : : : : : : : : : : : : : : : 1
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.jung.char.ps.gz, 19930927 A New Characterization of Lambda Definability Achim Jung1 and Jerzy Tiuryn 2 1 Fachbereich Mathematik, Technische Hochschule Darmstadt, Schlossgartenstrasse 7, D-6100 Darmstadt, Germany, jung@mathematik.th-darmstadt.de 2 Instytut Informatyki, Uniwersytet Warszawski, ul. Banacha 2, PL-02-097 Warszawa,
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.haack.hyper.ps.gz, 19930927 Die Hyperlimeskonstruktion Christian Haack August 1993 Diplomarbeit am Fachbereich Mathematik der Technischen Hochschule Darmstadt Betreuender Professor: Prof. Klaus Keimel Inhaltsverzeichnis 1 Einleitung 1 1.1 Vorgeschichte : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.winskel.mfcs-pb.ps.gz, 19930927 Completeness Results for Linear Logic on Petri Nets Uffe Engberg Glynn Winskel Computer Science Department Aarhus University Ny Munkegade DK-8000 Aarhus C, Denmark
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.abramsky.gfc.ps.gz, 19930927 Games and Full Completeness for Multiplicative Linear Logic Samson Abramsky and Radha Jagadeesan Department of Computing Imperial College of Science, Technology and Medicine Technical Report DoC 92/24 September 27, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.HO.dgis.ps.gz, 19930927 Dialogue Games and Innocent Strategies: An Approach to (Intensional) Full Abstraction for PCF Preliminary Announcement Martin Hyland and Luke Ong 26th July 1993 This note is (intended to be) released in conjunction with a preliminary announcement of Abramsky, Jagadeesan and Malacaria entitled Games and
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.pitts.evallogic.ps.gz, 19930927 Evaluation Logic Andrew M. Pittsy University of Cambridge Computer Laboratory Cambridge CB2 3QG England
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.jung.handbook.ps.gz, 19930927 Contents 1 Introduction and overview 6 1.1 General : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 1.2 Cartesian closure : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 1.3 Existence of fixpoints : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 1.4 Recursive
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.sunderhauf.nets.ps.gz, 19930927 QUASI-UNIFORM COMPLETENESS IN TERMS OF CAUCHY NETS PHILIPP S UNDERHAUF March 29, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.pitts.coinduction.ps.gz, 19930927 A Co-induction Principle for Recursively Defined Domains1 Andrew M. Pitts University of Cambridge Computer Laboratory New Museums Site, Pembroke Street Cambridge CB2 3QG, England hAndrew.Pitts@cl.cam.ac.uki 1To appear in Theoretical Computer Science
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.abramsky.gfapcf.ps.gz, 19930927 Games and Full Abstraction for PCF: Preliminary Announcement Samson Abramsky, Radha Jagadeesan and Pasquale Malacaria July 23, 1993 The Full Abstraction Problem for PCF is one of the longest-standing problems in the semantics of programming languages. There is quite widespread agreement
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.moggi.elt2.ps.gz, 19930927 A General Semantics for Evaluation Logic Eugenio Moggi September 15, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.moggi.mod-sem.ps.gz, 19930927 A Syntactic Approach to Modularity in Denotational Semantics Pietro Cenciarelli Dept. of Comp. Sci., Univ. of Edinburgh, UK, email: pic@dcs.ed.ac.uk Eugenio Moggi DISI, Univ. di Genova, ITALY, email: moggi@disi.unige.it
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.moggi.filter2.ps.gz, 19930927 A note on SDT in Filter Spaces Working Draft Eugenio Moggi September 5, 1993 Introduction This work was motivated by the desire to integrate Evaluation Logic ELT (see ) and Synthetic Domain Theory SDT (see ). A first step in this direction was to consider several computational monads over
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.ong.handbook.ps.gz, 19930927 Submitted to Handbook of Theoretical Computer Science Vol. 3, edited by S. Abramsky, D. Gabbay and T. S. E. Maibaum, Oxford University Press. Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF (Preliminary Version) C.-H. Luke Ong1 Computer Laboratory,
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.pitts.sipl.ps.gz, 19930927 On the Observable Properties of Higher Order Functions that Dynamically Create Local Names (preliminary report) Andrew Pitts1 Ian Stark2 University of Cambridge Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, England Tel: +44 223 334629 Fax: +44 223 334678 Email:
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.sunderhauf.qufsp.ps.gz, 19930927 Constructing a Quasi-Uniform Function Space Philipp S underhauf Fachbereich Mathematik, Arbeitsgruppe 1 Technische Hochschule Darmstadt Schlossgartenstrasse 7 D{64289 Darmstadt Germany e-mail: sunderhauf@mathematik.th-darmstadt.de February 16, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.jung.pcf.ps.gz, 19930927 Studying the Fully Abstract Model of PCF within its Continuous Function Model Achim Jung1 and Allen Stoughton2 Abstract. We give a concrete presentation of the inequationally fully abstract model of PCF as a continuous projection of the inductively reachable subalgebra of PCF's continuous function
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.schalk.pc.ps.gz, 19930927 Algebras for Generalized Power Constructions Vom Fachbereich Mathematik der Technischen Hochschule Darmstadt zur Erlangung des akademischen Grades eines Doktors der Naturwissenschaften (Dr. rer. nat.) genehmigte Dissertation von Dipl.-Math. Andrea Schalk aus Witten/Ruhr Referent: Prof. Dr. K. Keimel
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.stark.ps.gz, 19930927 A Calculus for Dynamic Allocation of Store Ian Stark. January 21, 1993. The Store-calculus is an extension of the call by value typed lambda calculus to allow the dynamic creation and use of typed storage. It is similar to the nu-calculus, which does the same for dynamic generation of names. The
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.abramsky.gfapcf2.ps.gz, 19930927 Games and Full Abstraction for PCF II: Second Preliminary Announcement Samson Abramsky, Radha Jagadeesan and Pasquale Malacaria September 8, 1993 In a previous note, we described how a certain category of games and strategies gave rise to an intensionally fully abstract model of PCF. We also explained
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.pitts.mfcs.ps.gz, 19930927 Observable Properties of Higher Order Functions that Dynamically Create Local Names, or: What's new Andrew M. Pitts and Ian D. B. Stark University of Cambridge Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, England
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.pitts.mfps.ps.gz, 19930927 Computational Adequacy via `Mixed' Inductive Definitions Andrew M. Pitts University of Cambridge Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, England
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.moggi.elt.ps.gz, 19930927 A Semantics for Evaluation Logic (extended version) Eugenio Moggi DISI, Univ. of Genova, Italy moggi@disi.unige.it July 29, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.lafont.finiteness.ps.gz, 19930928 A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier) Yves LAFONT CNRS Laboratoire de Math ematiques Discr etes September 15, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.pitts.rprd.ps.gz, 19930928 Relational Properties of Recursively Defined Domains Andrew M. Pitts University of Cambridge Computer Laboratory Cambridge CB2 3QG, UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/ta.ps.gz, 19930928 CLICS II Categorical Logic in Computer Science II Project Number: 6811 Technical Annex 1 Chapter I Description of the Project I-1 Project number, title and acronym Project number 6811 Title of the project Categorical Logic in Computer Science II Acronym CLICS-II I-2 Synopsis (* See next page *) 2 6811
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.lafont.equational.ps.gz, 19930928 Equational reasoning with 2-dimensional diagrams (preliminary version) Yves LAFONT Laboratoire d'Informatique Ecole Normale Sup erieure (URA 1327 du CNRS) July 29, 1992
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.winskel.handbook.ps.gz, 19930928 MODELS FOR CONCURRENCY (Draft copy of September 21, 1993) Glynn Winskel Mogens Nielsen Computer Science Department, Aarhus University, Denmark Contents 1 Introduction 3 2 Transition systems 8 2.1 A category of transition systems : : : : : : : : : : : : : : : : : : 8 2.2 Constructions on transition
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.winskel.lics93.ps.gz, 19930928 Bisimulation and open maps Andr e Joyal, Mogens Nielsen, Glynn Winskel Dep.de math.et d'info., Comp. Sc. Dept., Comp. Sc. Dept., U.Q.A.M., Univ. of Aarhus, Univ. of Aarhus, Montreal, Aarhus, Aarhus, Canada Denmark Denmark
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.aczel.Schematic.ps.gz, 19931004 Schematic Consequence Peter Aczel Manchester University
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.robinson.isos.ps.gz, 19931004 UNIVERSITY OF SUSSEX COMPUTER SCIENCE Parametricity as Isomorphism Edmund Robinson Report 5/92 September 1993 Computer Science School of Cognitive and Computing Sciences University of Sussex Brighton BN1 9QH ISSN 1350 3170 Parametricity as Isomorphism Edmund Robinson Abstract. We investigate a simple
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.aczel.Galois.ps.gz, 19931004 Galois: A Theory Development Project Peter Aczel Departments of Computer Science and Mathematics Manchester University, Manchester M13 9PL, U.K. September 28, 1993 A report on work in progress, for the Turin meeting on the Representation of Mathematics in Logical frameworks, January 20-23, 1993 1 The
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/ppr1.ps.gz, 19931004 CLICS II Categorical Logic in Computer Science II Basic Research Action Project Number: 6811 1st Periodic Progress Report October 8th, 1993 DRAFT { DO NOT DISTRIBUTE Contents 1 Executive summary 3 1.1 Milestones and Deliverables : : : : : : : : : : : : : : : : : : : : : : : : : 3 1.2 External Contacts :
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.rosolini.reflpar.ps.gz, 19931004 Reflexive graphs and parametric polymorphism G. Rosolini Dipartimento di Matematica via L.B. Alberti 4, 16132 Genova, Italy September 24, 1993 PRELIMINARY DRAFT Polymorphism enforces a type discipline on the normalizing terms of the >=-calculus and its many extensions intend to improve the intuition
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/clics/clics.taylor.sdtdual.ps.gz, 19931004 Stone Duality in Synthetic Domain Theory Paul Taylor, Department of Computing, Imperial College, London SW7 2BZ +44 71 589 5111 ext. 5057 1 October 1993 Synthetic domain theory has been guided so far by the slogan that domains are sets and all functions are continuous. Taken literally,
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/gfcsmallpagefinalversion.ps.gz, 19931201 Games and Full Completeness for Multiplicative Linear Logic Samson Abramsky and Radha Jagadeesan Department of Computing Imperial College of Science, Technology and Medicine December 1, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/tacs94.ps.gz, 19940104 Full Abstraction for PCF (Extended Abstract) Samson Abramsky and Pasquale Malacaria Imperial College Radha Jagadeesan Loyola University 1 Introduction The Full Abstraction Problem for PCF is one of the longeststanding problems in the semantics of programming languages. There is quite
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/nfgifinalversion.ps.gz, 19940105 New Foundations for the Geometry of Interaction Samson Abramsky Radha Jagadeesan Dept. of Computing Dept. of Mathematical Sciences Imperial College Loyola University London Chicago January 5, 1994 This research was supported by grants from UK SERC and ESPRIT Basic Research Action 3003 CLICS" 1 Contents
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/icI.ps.gz, 19940114 Interaction Categories Samson Abramsky Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate, London SW7 2BZ, England sa@doc.ic.ac.uk May 28, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/iccsp.ps.gz, 19940114 Chapter 1 Interaction Categories and Communicating Sequential Processes Samson Abramsky 1.1 Introduction The first lectures I heard on concurrency were given by Tony Hoare as part of a summer school held at the University of California at Santa Cruz in August 1979. The contents of those lectures are
	ftp://theory.doc.ic.ac.uk/theory/papers/Malacaria/bis.ps.gz, 19940208 Studying equivalences of transition systems with algebraic tools Pasquale Malacaria LIENS-DMI, Ecole Normale Superieure, 45 Rue d'Ulm, 75005 Paris, FRANCE email: pasquale@dmi.ens.fr
	ftp://theory.doc.ic.ac.uk/theory/papers/Finger/thesis.ps.gz, 19940322 Department of Computing Imperial College of Science, Technology and Medicine University of London Changing the Past: Database Applications of Two-Dimensional Temporal Logics Marcelo Finger February 1994 A thesis submited for the degree of Doctor of Philosophy of the University of London
	ftp://theory.doc.ic.ac.uk/theory/papers/Finger/two-dimension.ps.gz, 19940323 Handling Database Updates in Two-dimensional Temporal Logic Marcelo Finger y Department of Computing, Imperial College 180 Queen's Gate London SW7 2BZ, UK E-mail:mf3@doc.ic.ac.uk February 17, 1993 (Draft version 0.2)
	ftp://theory.doc.ic.ac.uk/theory/papers/Finger/adding.ps.gz, 19940323 Adding a temporal dimension to a logic system MARCELO FINGER and DOV M. GABBAY Imperial College, Department of Computing January 11, 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Finger/combining.ps.gz, 19940323 Combining Temporal Logic Systems Marcelo Finger Dov Gabbay Imperial College, Department of Computing 180 Queen's Gate London SW7 2BZ, UK mf3@doc.ic.ac.uk dg@doc.ic.ac.uk Draft version 17 March 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Finger/updating.ps.gz, 19940323 Updating Atomic Information in Labelled Database Systems (Extended Abstract) Marcelo Finger Dov M. Gabbay Department of Computing, Imperial College London SW7 2AZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/pasp.ps.gz, 19940415 Proofs as Processes Samson Abramsky April 14, 1994 The main purpose of this short paper is to serve as an introduction to the following paper, On the ss-calculus and Linear Logic", by Gianluigi Bellin and Philip Scott. The circumstances from which it arises are as follows. In June 1991 I gave a lecture
	ftp://theory.doc.ic.ac.uk/theory/papers/Lamarche/LinGamSeq.ps, 19940426 Sequentiality, Games and Linear Logic Fran cois Lamarche (The final version of this paper will contain an additional chapter on variants of the exponentials) March 25, 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Lamarche/prfnet1.ps, 19940426 Proof Nets for Intuitionistic Linear Logic I: Essential Nets Preliminay report Fran cois Lamarche April 26, 1994 In this series of two papers we present two classes of proof objects for intuitionistic linear logic with the connectives ; (;N and !1, which allows in particular the interpretation of the
	ftp://theory.doc.ic.ac.uk/theory/papers/Malacaria/tesi.ps.gz, 19940524 Semantica della riduzione del lambda calcolo: Dalle macchine ad ambienti alla geometria dell'interazione Tesi di dottorato Universit a di Torino Versione preliminare Pasquale Malacaria February 1, 1993 Contents 1 Introduzione 3 1.1 Riduzione del >= calcolo : : : : : : : : : : : : : : : : : : : : : : : 3
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/diss.ps, 19940916 Discrete Approximation of Spaces A Uniform Approach to Topologically Structured Datatypes and their Function Spaces Vom Fachbereich Mathematik der Technischen Hochschule Darmstadt zur Erlangung des akademischen Grades eines Doktors der Naturwissenschaften (Dr. rer. nat.) genehmigte Dissertation von
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/PhD.ps.gz, 19941007 `C >=K `ML `Myc q `R K `RE 3 `CD y O `CDVR >= `CDVP Y `CDV 3 `S ffi k oe `BCD `E s W `E `CE ISBN 90-9005752-8 Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/z++.ps, 19941025 The Z++ Manual K. Lano , H. Haughtony October 25, 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/parpoly.ps.gz, 19941031 Types, Abstraction, and Parametric Polymorphism, Part 2 QingMing Ma and John C. Reynolds School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA qingming.ma@cs.cmu.edu john.reynolds@cs.cmu.edu
	ftp://theory.doc.ic.ac.uk/theory/papers/McCusker/g4rt.ps.gz, 19941031 Games for recursive types Samson Abramsky and Guy McCusker Imperial College 13 October 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/normhard.ps.gz, 19941031 Even Normal Forms Can be Hard to Type John C. Reynolds1 Carnegie Mellon University Pittsburgh, Pennslyvania 15213 U.S.A. Extended Abstract \| December 1, 1989 1. Introduction Although type inference, in the form of the Hindley-Milner algorithm, has been successfully applied to languages with a simple
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/intcode.ps.gz, 19941031 Using Functor Categories to Generate Intermediate Code John C. Reynolds Department of Computing Imperial College London SW7 2BZ, Great Britain jr@doc.ic.ac.uk School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA john.reynolds@cs.cmu.edu
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/polyintro.ps.gz, 19941031 This is a preprint of the introduction to the section on Polymorphic Lambda Calculus" in Logical Foundations of Functional Programming, Proceedings of the Year of Programming Institute", edited by G erard Huet, to be published by Addison Wesley. An Introduction to the Polymorphic Lambda Calculus John
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/coherence.ps.gz, 19941031 1 The Coherence of Languages with Intersection Types John C. Reynolds School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890, USA john.reynolds@cs.cmu.edu
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/g4rt.ps.gz, 19941110 Games for recursive types Samson Abramsky and Guy McCusker Imperial College 13 October 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/sas94.ps.Z, 19941207 A Type-based Framework for Program Analysis Chris Hankin1 and Daniel Le M etayer2 1 Department of Computing, Imperial College, LONDON SW7 2BZ, UK 2 INRIA/IRISA, Campus de Beaulieu, 35042 RENNES CEDEX, FRANCE
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/popl94.ps.Z, 19941207 Deriving algorithms from type inference systems: Application to strictness analysis Chris Hankin Department of Computing, Imperial College, LONDON SW7 2BZ, UK Daniel Le M etayer INRIA/IRISA Campus de Beaulieu 35042 RENNES CEDEX, FRANCE
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/esop94.ps.Z, 19941207 Lazy type inference for the strictness analysis of lists Chris Hankin1 and Daniel Le M etayer2 1 Department of Computing, Imperial College, LONDON SW7 2BZ, UK 2 INRIA/IRISA, Campus de Beaulieu, 35042 RENNES CEDEX, FRANCE
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/forsytheintro.ps.gz, 19941212 This paper is based on lectures given at the DARPA/ISTO Software Principal Investigators Meeting, Providence, Rhode Island, February 27, 1991, and the University of Illinois, April 4, 1991. Replacing Complexity with Generality: The Programming Language Forsythe John C. Reynolds Carnegie Mellon
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/functexp.ps.gz, 19941212 This is a preprint of a paper that has been submitted to Information and Computation. On Functors Expressible in the Polymorphic Typed Lambda Calculus John C. Reynolds Carnegie Mellon University and Gordon D. Plotkiny University of Edinburgh January 22, 1991
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/forsytherep.ps.gz, 19941212 Preliminary Design of the Programming Language Forsythe John C. Reynolds1 Carnegie Mellon University June 21, 1988 CMU-CS-88-159
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/syncontrol.ps.gz, 19941212 Syntactic Control of Interference Part 2 John C. Reynolds1 December 12, 1994 CMU-CS-89-130 School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 This is a preprint of a paper that will appear in the Proceedings of the 16th International Colloquium on Automata, Languages, and
	ftp://theory.doc.ic.ac.uk/theory/papers/Reynolds/histcont.ps.gz, 19941223 LISP AND SYMBOLIC COMPUTATION: An International Journal, 6, 233{247, 1993 c 1993 Kluwer Academic Publishers { Manufactured in The Netherlands The Discoveries of Continuations JOHN C. REYNOLDS (John.Reynolds@cs.cmu.edu) School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/gamma.ps.Z, 19950119 Compositional semantics of a notation for composing parallel programs Chris Hankin Daniel Le M etayery David Sandsz
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/rssr.ps, 19950120 Reactive System Specification and Refinement K. Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ.
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/marktoberdorf.ps.gz, 19950124 Interaction Categories and the Foundations of Typed Concurrent Programming Samson Abramsky, Simon Gay and Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7 2BZ, UK. email: fsa,sjg3,rn4g@doc.ic.ac.uk Tutorial notes on Samson
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/fixpoints.ps.gz, 19950209 On Gabbay's temporal fixed point operator Ian Hodkinson 8 December 1993
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/finvar.ps.gz, 19950213 Finite variable logics Ian Hodkinson Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ, England. Email: imh@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/93_12_duarte.ps.gz, 19950221 T ecnicas Formais e Informais: Um Estudo sobre Integra c~ao usando Statecharts Carlos Henrique C. Duarte Edward H. Haeusler @inf.puc-rio.br Departamento de Inform atica Pontif cia Universidade Cat olica do Rio de Janeiro R. Marqu^es de S. Vicente, 225, Rio de Janeiro, RJ, 22453, Brazil
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/msc.ps.gz, 19950221 Carlos Henrique Cabral Duarte O desenvolvimento de um compilador MIRANDA usando um m etodo orientado a objetos Disserta c~ao apresentada ao Departamento de Inform atica da PUC/RJ como parte dos requisitos para obten c~ao do t tulo de Mestre em Ci^encia da Computa c~ao Orientador: Prof. Roberto
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/92_33_duarte.ps.gz, 19950221 On the Modularization of Formal Specifications: The NDB Example Revisited C. H. C. Duarte R. Ierusalimschy C. J. P. Lucena @inf.puc-rio.br Departamento de Inform atica Pontif cia Universidade Cat olica do Rio de Janeiro R. Marqu^es de S. Vicente, 225, Rio de Janeiro, RJ, 22453,
	ftp://theory.doc.ic.ac.uk/theory/papers/Hirsch/cr.ps, 19950316 Complete Representations in Algebraic Logic Robin Hirsch & Ian Hodkinson February 2, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Hirsch/notes.ps, 19950316 Axiomatising various classes of relation and cylindric algebras Robin Hirsch, Ian Hodkinson February 2, 1995 Part I Representations 1 Introduction Relation algebras are to binary relations what boolean algebras are to unary ones. They are used in artificial intelligence, where (e.g.) the Allen{Koomen
	ftp://theory.doc.ic.ac.uk/theory/papers/ReynoldsM/afotl.ps.Z, 19950316 Axiomatising First-Order Temporal Logic: Until and Since over Linear Time Mark Reynolds1 February 17, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/lics95.ps.gz, 19950407 To appear in proceedings of 10th annual IEEE symposium on Logic in Computer Science, June 1995. Games and Full Abstraction for the Lazy >=-calculus Samson Abramsky Guy McCusker Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/main.ps, 19950407 Specification Structures and Propositions-as-Types for Concurrency Samson Abramsky Simon Gay Rajagopal Nagarajan
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/psevdm_paper.ps.Z, 19950412 Specifying Discrete Event Systems in VDM++ K. Lano, S. Goldsack1
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/strict95.ps.gz, 19950425 Possible and Guaranteed Concurrency in CSP Marta Kwiatkowska School of Computer Science, University of Birmingham Edgbaston, Birmingham B15 2TT, UK Iain Phillipsy Department of Computing, Imperial College 180 Queens Gate, London SW7 2BZ, UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Hirsch/step.ps, 19950515 Step by Step - Building Representations in Algebraic Logic Robin Hirsch & Ian Hodkinson Department of Computing, 180 Queens Gate, London, SW7 2BZ May 15, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/ReynoldsM/csall.ps.Z, 19950516 MetateM in Intensive Care M Reynolds1 Department of Computing Imperial College London September 12, 1994 DRAFT
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/infcat.ps.Z, 19950518 Information Categories Abbas Edalat Michael B. Smyth Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ England.
	ftp://theory.doc.ic.ac.uk/theory/papers/ReynoldsM/tgs.ps.Z, 19950518 Temporal Semantics for Gamma Mark Reynolds1 Department of Computing Imperial College May 18, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/neuralmfps.ps.Z, 19950518 Electronic Notes in Computer Science 1 (1995) Domain Theory in Learning Processes A. Edalat 1 Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Clark/value_passing.ps.Z, 19950522 Static Analysis of Value-Passing Process Calculi (Extended Abstract) David Clark, Lindsay Errington and Chris Hankin
	ftp://theory.doc.ic.ac.uk/theory/papers/Clark/alag.ps.gz, 19950522 A Lattice of Abstract Graphs David Clark and Chris Hankin Dept. of Computing Imperial College of Science,Technology and Medicine 180 Queen's Gate, LONDON SW7 2BZ, UK Abstract. This paper concerns the abstract interpretation of Term Graph Rewriting systems. We introduce a new lattice of abstract graphs;
	ftp://theory.doc.ic.ac.uk/theory/papers/Finger/maindms.ps.gz, 19950522 Updating Atomic Information in Labelled Database Systems (Extended Abstract) Marcelo Finger Dov M. Gabbay Department of Computing, Imperial College London SW7 2AZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/hs.ps.gz, 19950526 The k-variable property is stronger than H-dimension k Ian Hodkinson Andr as Simony
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/int.ps.Z, 19950608 Domain Theory and Integration Abbas Edalat Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/stochlicsf.ps.Z, 19950608 Domain Theory in Stochastic Processes Abbas Edalat Department of Computing, Imperial College, London SW7 2BZ. ae@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/powerf.ps.Z, 19950608 Power Domains and Iterated Function Systems Abbas Edalat Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/misc/curric.ps.gz, 19950609 Curriculum Vitae Todas as informa c~oes contidas neste documento s~ao verdadeiras e podem ser comprovadas se necess ario atrav es de documentos apropriados ou por pessoas de refer^encia. Carlos Henrique Cabral Duarte 9 de Junho de 1995 Curriculum Vitae - Carlos H. C. Duarte 1 1 - Identifica c~ao 1.
	ftp://theory.doc.ic.ac.uk/theory/papers/Clark/savpc.ps.Z, 19950714 STATIC ANALYSIS OF VALUE-PASSING PROCESS CALCULI (Extended Abstract) DAVID CLARK, LINDSAY ERRINGTON and CHRIS HANKIN Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: fdjc2, le, clhg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Clark/spntgr.ps.Z, 19950714 Electronic Notes in Theoretical Computer Science 1 (1995) to appear Some Properties of Non-Orthogonal Term Graph Rewriting David Clark Department of Computing Imperial College London, UK Richard Kennaway 1 Department of Information Systems University of East Anglia Norwich, UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/kz.ps.gz, 19950718 CONSTRUCTING SPECIFICATIONS AND MODULES IN A KZ-DOCTRINE GILLIAN HILL Department of Computer Science, City University Northampton Square, London, EC1 VOH B E-mail: gah@cs.city.ac.uk and Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: gah@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/AMAST93.ps.gz, 19950718 Category Theory for the Configuration of Complex Systems Gillian Hill Department of Computing, Imperial College of Science and Technology and Department of Computer Science, City University, London, Great Britain
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/cast94.ps.gz, 19950718 The Configuration of Complex Systems Gillian Hill Department of Computing, Imperial College of Science, Technology and Medicine Department of Computer Science, City University, London, Great Britain
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/cast95.ps.gz, 19950718 A Logical Approach to System Construction Gillian Hill Department of Computer Science, City University and Department of Computing, Imperial College of Science, Technology and Medicine, London, Great Britain
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/lics95.ps.gz, 19950725 In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, 1995. A Typed Calculus of Synchronous Processes Simon Gay Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/marktoberdorf.ps.gz, 19950725 Deductive Program Design: Proceedings of the 1994 Marktoberdorf Summer School. NATO ASI Series F, Springer-Verlag, 1995. Interaction Categories and the Foundations of Typed Concurrent Programming Samson Abramsky, Simon Gay and Rajagopal Nagarajan Department of Computing, Imperial College of Science,
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/sorting.ps.gz, 19950725 A Sort Inference Algorithm for the Polyadic ss-Calculus Simon J. Gay Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London, UK SW7 2BZ hsjg3@doc:ic:ac:uki October 28, 1992
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/banff.ps.gz, 19950725 Specification Structures and Propositions-as-Types for Concurrency Samson Abramsky Simon Gay Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, London, UK. email: fsa,sjg3,rn4g@doc.ic.ac.uk.
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/thesis.ps.gz, 19950725 Logical Considerations in the Interpretation of Presuppositional Sentences Pablo Gerv as G omez{Navarro Department of Computing Imperial College of Science, Technology and Medicine University of London A thesis submitted for the degree of Doctor of Philosophy of the University of London and for the
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/intlang.ps.gz, 19950725 Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, Imperial College Press, 1995. AN INTERNAL LANGUAGE FOR INTERACTION CATEGORIES ROY CROLE Department of Mathematics and Computer Science, University of Leicester
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/modsic.ps.gz, 19950725 Modelling Signal in Interaction Categories Simon Gay and Rajagopal Nagarajan fsjg3,rn4g@doc.ic.ac.uk Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/nets.ps.gz, 19950727 Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, Imperial College Press, 1995. COMBINATORS FOR INTERACTION NETS SIMON GAY Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/gamma.ps.gz, 19950727 A Program Logic for Gamma S. J. Gay and C. L. Hankin Department of Computing, Imperial College of Science, Technology and Medicine, London, UK June 23, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/GeoZ.ps.gz, 19950728 GEOMETRIC LOGIC AS A SPECIFICATION LANGUAGE STEVEN VICKERS Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: sjv@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/Toolkit.ps.gz, 19950728 TOWARDS A GeoZ TOOLKIT MARK DAWSON and STEVEN VICKERS Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: fmd,sjvg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/lnp.ps.gz, 19950728 LOCALES ARE NOT POINTLESS STEVEN VICKERS Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: sjv@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lamarche/LICS95.ps, 19950731 Games Semantics for Full Propositional Linear Logic Fran cois Lamarche Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, UK. gfl@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lamarche/gencohMFPS.ps, 19950731 Electronic Notes in Theoretical Computer Science 1 (1995) to appear Generalizing Coherence Spaces and Hypercoherences Fran cois Lamarche Department of Computing Imperial College 180 Queen's Gate London SW7 UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Lamarche/cpo.ps, 19950809 FROM CHU SPACES TO CPOS FRANC OIS LAMARCHE Laboratoire de Math ematiques Discr etes UPR9016, 163 Avenue de Luminy, case 930, Marseille cedex 9, France E-mail: lamarche@lmd.univ-mrs.fr, gfl@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/sem.ps, 19950822 Reasoning and Refinement in VDM++ K. Lano, S. Goldsack August 22, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/drafts/spectrum.ps.gz, 19950825 THE CHALLENGE FORTHE CHALLENGE FOR Brazilian software eBrazilian software efffortsforts CARLOS H. C. DUARTE National Bank of Social and Economic Development ince the eighties, astonishing changes have taken place within the computing industry in Brazil. Rather than the so-called market reserve system
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/TopPLN.ps, 19950906 Toposes pour les nuls Steve Vickers Imperial College Introduction The very first sentence of Mac Lane and Moerdijk says: A topos can be considered both as a generalized space" and as a generalized universe of sets". The generalized universe of sets" aspect of toposes is relatively easy to
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/dmfv.ps.Z, 19950919 Dynamical systems, Measures and Fractals via Domain Theory Abbas Edalat Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/project.ps, 19950925 Description Of the Research Project To be carried out at the host institution FORM A L SOFTW A RE D E VELOPM E NT=SYNTH E SIS ( A Formal approach to Automated Software Engineering ) July 14, 1995 2 Description Of the Research Project 3 Introduction At the heart of the software problem lies the lack of
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/cpimtr-ab.ps.Z, 19950925 Implementations underlie the refinement of logical specifications" and provide the foundations for program development, data type refinement, algorithm and data structure design. An implementation may invoke the need to provide some additional support, necessary for the representation of the abstract
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/fyrep.ps.Z, 19950925 Formal Program Development Constructive Techniques (Report Summary) Theodosis G. Dimitrakos Department of Computing Imperial College of Science,Technology and Medicine e-mail: td@doc.ic.ac.uk December 20, 1994 Chapter 1 Introduction Algorithm design, program development and program/data-type refinement
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/misc/report1.ps.gz, 19951002 Carlos Henrique Cabral Duarte First Year Report Supervisor: Prof. T. S. E. Maibaum Period: October/1994 to September/1995 DEPARTMENT OF COMPUTING IMPERIAL COLLEGE OF SCIENCE, TECHNOLOGY AND MEDICINE October 2, 1995 1 Introduction The present document reports the first year of studies of Carlos Henrique
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/wadt95-slides.ps.Z, 19951002 On the construction of primitive implementations for logical specifications presented by T. Dimitrakos Dpt of Computing Imperial College SW7 2BZ U.K. WADT 95 WADT 95 Implementation Triangle Source specification: All properties of the source should be respected and mirrored properly in the
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/FROCOS/PMLDS.ps, 19951012 Generalising Propositional Modal Logic Using Labelled Deductive Systems Alessandra Russo Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BX, U.K. ar3@doc.ic.ac.uk October 1995 A submission to the First International Workshop on Frontiers of Combining Systems (FroCoS'96)
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/TECH_REPORT/modalLDS.ps, 19951016 Modal Labelled Deductive Systems Imperial College Research Report DoC 95/7 Alessandra Russo Department of Computing Imperial College of Science, Technology and Medicine, 180, Queen's Gate, London SW7 2BZ England, email: ar3@doc.ic.ac.uk March 1995 Last revision October 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/powerpoints.ps, 19951017 Constructive points of Powerlocales Steven Vickers Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ sjv@doc.ic.ac.uk October 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/atomstrs.ps.gz, 19951024 Atom structures of relation algebras Ian Hodkinson October 24, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/EROS/eros_subcomp.ps.Z, 19951031 Inheritance, Subtyping and Refinement in Object-oriented Specification and Programming Languages K. Lano October 31, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/VPP/ProdCell/klaus.ps, 19951119 A Comparison of B AMN and VDM++ on the `Production Cell' Case Study K. Lano1
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/step.ps.gz, 19951201 Step by Step \| Building Representations in Algebraic Logic Robin Hirsch & Ian Hodkinson December 1, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Malacaria/PCFfullabs.ps.Z, 19951207 Full Abstraction for PCF Samson Abramskyy Radha Jagadeesanz Pasquale Malacariax December 7, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/banff.ps.gz, 19951207 Specification Structures and Propositions-as-Types for Concurrency Samson Abramsky Simon Gay Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, London, UK. email: fsa,sjg3,rn4g@doc.ic.ac.uk.
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/PCFfullabs.ps.Z, 19951207 Full Abstraction for PCF Samson Abramskyy Radha Jagadeesanz Pasquale Malacariax December 7, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/sync_discuss.ps.Z, 19951207 Subtyping, Refinement and Synchronisation K. Lano, S. Goldsack December 7, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/realpcf.ps.gz, 19951208 PCF extended with real numbers Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, United Kingdom, E-mail: mhe@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/integrationpcf.ps.gz, 19951208 Integration in Real PCF Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College, London SW7 2BZ fae,mheg@doc.ic.ac.uk 1 Introduction Traditionally, in computing science one represents real numbers by floating-point approximations. If we assume that these approximations are exact"
	ftp://theory.doc.ic.ac.uk/theory/papers/McCusker/fpc.ps.gz, 19951208 Games and Full Abstraction for fpc Guy McCusker Imperial College, University of London
	ftp://theory.doc.ic.ac.uk/theory/papers/Bucciarelli/logrel.ps.Z, 19951211 Logical relations and >=-theories Antonio Bucciarelli Departement of Computing, Imperial College, London e-mail:abb1@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Bucciarelli/quotient.ps.Z, 19951211 Logical reconstruction of bi-domains extended abstract Antonio Bucciarelli
	ftp://theory.doc.ic.ac.uk/theory/papers/Bucciarelli/degrees.ps.Z, 19951211 Degrees of parallelism in the continuous type hierarchy Antonio Bucciarelli LIENS-DMI, Ecole Normale Sup erieure, 45 rue d'Ulm, Paris, France A degree of parallelism is an equivalence class of Scott-continuous functions which are relatively definable by each other with respect to the language PCF (a
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/bcs95.ps.Z, 19951214 Categorial Semantics for Object-oriented Specification K. Lano, J. Fiadeiro, S. Goldsack December 14, 1995 This paper will outline a semantics for concurrent and real-time object-oriented specification languages such as VDM++ and Z++ and identify the role played by category-theoretic concepts in
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/draft1.ps.Z, 19960102 The implementation of PO-specifications Theodosis Dimitrakos Department of Computing Imperial College of Science,Technology and Medicine e-mail: td@doc.ic.ac.uk January 2, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/refmethod.ps.Z, 19960112 A methodological approach to the refinement of logical specifications Status: Extended Abstract Theodosis Dimitrakos January 12, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/handbook.ps, 19960115 Domain Theory Samson Abramsky and Achim Jung Contents 1 Introduction and Overview : : : : : : : : : : : : : : : : : : : : 2 1.1 Origins : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2 1.2 Our approach : : : : : : : : : : : : : : : : : : : : : : : : 4 1.3 Overview : : : : : : : : : : : : : : :
	ftp://theory.doc.ic.ac.uk/theory/papers/McCusker/lics95.ps.gz, 19960117 In proceedings of 10th annual IEEE symposiumon Logic in Computer Science, IEEE Computer Society Press, June 1995. Games and Full Abstraction for the Lazy >=-calculus Samson Abramsky Guy McCusker Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch1-2.ps.gz, 19960126 1 Computability, Algorithms and Complexity Nominally 20 lectures Ian Hodkinson Department of Computing Imperial College 180 Queen's Gate London SW7 2BZ UK email imh@doc.ic.ac.uk) Introduction This course has three parts: I: computability theory, II: algorithms, III: complexity theory. In Part I we
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch9-10.ps.gz, 19960126 122 CS240 Part III: Complexity theory Introduction In part I of the course we saw that some problems are algorithmically unsolvable. Eg: the halting problem (will a given TM halt on a given input ) deciding the truth of an arbitrary statement about arithmetic. But there are wide variations in difficulty
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/Information.ps.gz, 19960126 i Computability, Algorithms and Complexity Ian Hodkinson 1996 Department of Computing, Imperial College, London SW7 2BZ, UK. Contents Books and other reading .............................................................................. iv Introduction
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch4-5.ps.gz, 19960126 54 4. Universal Turing machines We nowadays accept that a single computer can solve a vast range of problems, ranging from astronomical calculations to graphics and process control. But before computers were invented there were many kinds of problem-solving machines, with quite different hardware .
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch11-12.ps.gz, 19960126 142 11 Reduction in p-time We now use Turing machines to formalise the technique we saw in 8.6 of reducing one problem to another in p-time. This p-time reduction gives fast non-deterministic solutions to new yes/no problems from known fast nondeterministic solutions to old ones. We'll study its
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch3.ps.gz, 19960126 36 3. Variants of Turing machines In this section we examine some variants of the TM we considered before. The main examples we have in mind are machines with a two-way infinite tape, or more than one tape. We will see that in computational power they are all the same as the ordinary model. This is in
	ftp://theory.doc.ic.ac.uk/theory/papers/DAgostino/taming.ps.Z, 19960201 The Taming of the Cut. Classical Refutations with Analytic Cut Marcello D'Agostino Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ (England) mda@uk.ac.ic.doc Marco Mondadori Istituto di Discipline Filosofiche Universit a di Ferrara via Savonarola 38, 44100 Ferrara (Italy)
	ftp://theory.doc.ic.ac.uk/theory/papers/DAgostino/tableaux.ps.Z, 19960201 Are Tableaux an Improvement on Truth-Tables Cut-Free proofs and Bivalence Marcello D'Agostino Department of Computing Imperial College 180 Queen's Gate London SW7 2BZ mda@uk.ac.ic.doc 12 February 1992
	ftp://theory.doc.ic.ac.uk/theory/papers/DAgostino/popper.ps.Z, 19960201 KRYSIA BRODA MARCELLO D'AGOSTINO MARCO MONDADORI A SOLUTION TO A PROBLEM OF POPPER
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/tsvslides.ps, 19960209 Theory of Specification and Verification Topics: ffl Specification in B (weeks 1 to 5) { kcl; ffl Object Calculus (weeks 6 to 10) { tsem. Comprehensive introduction to formal meth- ods" and their use in specification and de- velopment. Emphasis on object-based or object-oriented methods. Books: B: An
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/seb.ps, 19960212 A Semantics for Syntropy ffl Syntropy { a fusion of OO methods and formal notation (Z); ffl Uses statecharts and events to abstract from message passing; ffl Three models: essential, specification and implementation. + 1 Specification Model Example Monitor price: Zbound: N Armed Alarmed Share monitor
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/TFMworkshopEA.ps, 19960220 From logical theories to PO-specifications Theodosis Dimitrakos Department of Computing Imperial College of Science,Technology and Medicine e-mail: td@doc.ic.ac.uk Extended Abstract The process of software development consists of theory manipulations. This assertion is able to provide an overview of
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/C_delta.ps.gz, 19960221 COUNTABLE PRODUCTS OF ABSOLUTE Cffi SPACES TILL PLEWE
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/pospecs.ps.Z, 19960226 From logical theories to PO-specifications Theodosis Dimitrakos Department of Computing Imperial College of Science,Technology and Medicine e-mail: td@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/TFMworkshop.ps, 19960226 From logical theories to PO-specifications Theodosis Dimitrakos Department of Computing Imperial College of Science,Technology and Medicine e-mail: td@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/FROCOS/Russo.ps.Z, 19960227 GENERALISING PROPOSITIONAL MODAL LOGIC USING LABELLED DEDUCTIVE SYSTEMS ALESSANDRA RUSSO Imperial College of Science, Technology and Medicine, Department of Computing, 180 Queen's Gate, London SW7 2BX, U.K. ar3@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/McCusker/translation.ps.gz, 19960301 Full abstraction by translation Guy McCusker 1 March 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/jose.ps, 19960303 Development of Concurrent Systems in B AMN K. Lano , J. Dicky March 1, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/marktoberdorf.ps.gz, 19960304 Deductive Program Design: Proceedings of the 1994 Marktoberdorf Summer School. NATO ASI Series F, Springer-Verlag, 1995. Interaction Categories and the Foundations of Typed Concurrent Programming Samson Abramsky, Simon Gay and Rajagopal Nagarajan Department of Computing, Imperial College of Science,
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/modsic.ps.gz, 19960304 Modelling Signal in Interaction Categories Simon Gay and Rajagopal Nagarajan fsjg3,rn4g@doc.ic.ac.uk Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/intlang.ps.gz, 19960304 Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, Imperial College Press, 1995. AN INTERNAL LANGUAGE FOR INTERACTION CATEGORIES ROY CROLE Department of Mathematics and Computer Science, University of Leicester
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/banff.ps.gz, 19960304 Specification Structures and Propositions-as-Types for Concurrency Samson Abramsky Simon Gay Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, London, UK. email: fsa,sjg3,rn4g@doc.ic.ac.uk.
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/lics95.ps.gz, 19960304 In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, 1995. A Typed Calculus of Synchronous Processes Simon Gay Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/typdf.ps.gz, 19960304 Types for Deadlock-Freedom Samson Abramsky Simon Gayy Rajagopal Nagarajanz
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/drafts/deli.ps.gz, 19960314 Exploiting Actors as an Extensible Language Extension Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom e-mail: cd7@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/fme96vdmslides.ps, 19960315 Formal Development of Object-oriented Systems in VDM++: FME 96 Tutorial Kevin Lano, Stephen Goldsack Dept. of Computing, Imperial College f kcl, sjg g@doc.ic.ac.uk ffl Object-oriented formal methods; ffl Industrial applications; ffl Formal OO development process; ffl Tool support; ffl Sequential
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/fme96slides.ps, 19960315 Formal Development in B Abstract Machine Notation: FME 1996 Tutorial Topics: 1. Key Concepts; 2. B AMN Specifications; 3. Semantics of B AMN; 4. Structuring Specifications; 5. Refinement; 6. Animation and Proof; 7. Implementation. Contact: kcl@doc.ic.ac.uk + 1 Key Concepts Requirements Specification
	ftp://theory.doc.ic.ac.uk/theory/papers/Dargam/dar96b-aismc3.ps, 19960315 Compromised Updates in Labelled Databases F atima C. C. Dargam e-mail: fccd@doc.ic.ac.uk Department of Computing Imperial College of Science, Technology and Medicine 180 Queens Gate, London SW7 2BZ United Kingdom 15 March 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/sosl.ps, 19960320 Developing Formal Semantics for Object-Oriented Specification Languages K. Lano March 19, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/ch6ps.ps, 19960321 Contents 6 Proof Methods and Techniques 176 6.1 Safety Reasoning { Monitor and Gate 176 6.2 Liveness Reasoning { Dining Philosophers 180 6.3 Internal Consistency Proofs 182 6.4 Refinement and Subtyping Proofs 183 6.5 Object Identity 207 6.6 Reasoning About Concurrent Object Execution 212 6.7
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/z92ps.ps, 19960321 Reuse and Adaptation of Z Specifications K. Lano Applied Information Engineering, Lloyd's Register 29 Wellesley Rd. Croydon CR0 2AJ H. Haughton Applied Information Engineering, Lloyd's Register 29 Wellesley Rd. Croydon CR0 2AJ
	ftp://theory.doc.ic.ac.uk/theory/papers/Dargam/thesis-draft.ps.Z, 19960321 On Reconciling Conflicting Updates (A Compromised Revision Approach) F atima Cristina Canazaro Dargam March 1996 ( Draft ) Department of Computing Imperial College of Science, Technology and Medicine University of London This thesis is submitted to the University of London in partial fulfillment of the
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/ch4ps.ps, 19960321 Contents 4 Specification Notations and Techniques 84 4.1 Attributes and Data Structures 85 4.2 Operations 92 4.3 Inheritance 111 4.4 Subtyping 113 4.5 Class Composition 120 4.6 Object Identity 122 4.7 Dynamic Behaviour 126 4.8 Complex Data Types 132 4.9 VDM++ 134 83 Chapter 4 Specification Notations and
	ftp://theory.doc.ic.ac.uk/theory/papers/Dargam/dar96c.ps.Z, 19960325 A Compromised Characterization to Belief Revision Imperial College Research Report DoC 96/2 F atima C. C. Dargam e-mail: fccd@doc.ic.ac.uk Department of Computing Imperial College of Science, Technology and Medicine 180 Queens Gate, London SW7 2BZ United Kingdom 25 March 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Dargam/dar96b.ps.Z, 19960325 On Compromising Updates in Labelled Databases Imperial College Research Report DoC 96/1 F atima C. C. Dargam e-mail: fccd@doc.ic.ac.uk Department of Computing Imperial College of Science, Technology and Medicine 180 Queens Gate, London SW7 2BZ United Kingdom 25 March 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/annealing.ps, 19960327 Refinement of object structures in VDM++ (Draft version: comments will be welcome: send to sjg@doc.ic.ac.uk) S.J. Goldsack and K Lano Imperial College, London E. D urr Cap Volmac, Utrecht, Netherlands. August 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/realpcf.ps.gz, 19960328 PCF extended with real numbers Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, United Kingdom, E-mail: mhe@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/integrationpcf.ps.gz, 19960328 Integration in Real PCF Abbas Edalat Mart n H otzel Escard o Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ, UK fae,mheg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/realinduc.ps.gz, 19960328 INDUCTION AND RECURSION ON THE REAL LINE MART IN H OTZEL ESCARD O Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: mhe@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/orl.ps.gz, 19960401 Mosaics and step-by-step \| Remarks on `A modal logic of relations' by Venema & Marx Robin Hirsch, Ian Hodkinson, Maarten Marx, Szabolcs Mikul as, and Mark Reynolds Mosaics were introduced by N emeti in , and developed further in . They are very useful in decidability and completeness proofs.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/mr1.ps, 19960401 Specifying Static Analysis Tools Using Formal Methods K. Lano Dept. of Computing Imperial College London SW7 2BZ, UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/mr2.ps, 19960401 Object-oriented Formal Development K. Lano, S. Goldsack Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/drafts/acid.ps.gz, 19960409 Acidity Yields Another Notion for Modularity in Formal Object-Oriented Specifications Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom e-mail: cd7@doc.ic.ac.uk 1 Introduction The use of transactions as a means of structuring and modularising
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/petef.ps, 19960416 EPSRC Information and Software Technology Project No: 4335-778FOT Formal Underpinnings for Object Technology (FOT) Semantic Frameworks for Syntropy 4335-778-2.006 Kevin Lano
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/TFMworkshop1996.ps.gz, 19960510 Gamma and the Logic of Transition Traces S. J. Gay C. L. Hankin Department of Computer Science, Department of Computing, Royal Holloway, University of London, Imperial College of Science, Egham, Surrey, UK Technology and Medicine, simon@dcs.rhbnc.ac.uk 180 Queen's Gate, London, UK clh@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/zedan.ps, 19960515 Refinement of Concur- rent Systems in VDM++ K. Lano and S. Goldsack DMU, May 1996 + 1 Topics ffl Refining Sequential Specifications to Concurrent/Distributed Implementations ffl VDM++ and Semantics ffl Annealing ffl Processes as Theories ffl Examples + 2 Refinement ffl Sequential specifications often
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/lrm.ps, 19960519 ESPRIT 6500 AFRODITE VDM++ Language Reference Manual Authorised by: Authors: E.H. D urr, N. Plat (editor) Cap Volmac Date: February 1995 Doc. ID: AFRO/CG/ED/LRM/V10 Afrodite in confidence Document type: Standard Status: Proposed Confidentiality: Afrodite in confidence Work Package allocation: WP-No.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/hong.ps, 19960522 Axioms for Object-Oriented Extensions to Z K. Lano H. Haughtony May 23, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/gam.ps, 19960526 EXTENDING B AMN WITH CONCURRENCY K. LANO Department of Computing, Imperial College, London SW7 2BZ. J. FIADEIRO Dept. of Informatics, Faculty of Sciences, University of Lisbon J. DICK B-Core (UK) Ltd., Oxford Science Park, Oxford OX4 4GA This paper outlines an approach to concurrent specification in B
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/rfrance.ps, 19960527 A Semantic Comparison of Fusion and Syntropy K. Lano, R. France May 27, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/mwg.ps, 19960529 Framework 4 1994-1998 Working Group Methodology for the Development of Computer System Specifications MeDiCiS Coordinator: Kevin Lano Department of Computing, Imperial College Proposal number: 1 Summary Summary (one page) The summary should concisely address the essence of the proposal: The activities
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/axiomatic.ps.gz, 19960530
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/CAAP92.ps.gz, 19960531 Partial Type Assignment in Left Linear Applicative Term Rewriting Systems Theory, Applications and Implementation. Steffen van Bakel1y Sjaak Smetsers1 Simon Brock2 1) Department of Informatics, Faculty of Mathematics and Informatics, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/TCS92-102.ps.gz, 19960531 Complete restrictions of the intersection type discipline Steffen van Bakel Department of Informatics, Faculty of Mathematics and Informatics, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands. e-mail: steffen@cs.kun.nl
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/TCS95-151.ps.gz, 19960531 Intersection Type Assignment Systems Steffen van Bakel Afdeling Informatica, Universiteit Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, Nederland. steffen@cs.kun.nl
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/JLC93-3-6.ps.gz, 19960531 Principal Type Schemes for the Strict Type Assignment System STEFFEN VAN BAKEL, Department of Informatics, Faculty of Mathematics and Informatics, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands. E-mail: steffen@cs.kun.nl
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/FSTTCS93.ps.gz, 19960531 Essential Intersection Type Assignment Steffen van Bakel Department of Informatics, Faculty of Mathematics and Informatics, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands. steffen@cs.kun.nl
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/TLCA93.ps.gz, 19960531 Partial Intersection Type Assignment in Applicative Term Rewriting Systems Steffen van Bakel Department of Informatics, Faculty of Mathematics and Informatics, University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, The Netherlands. steffen@cs.kun.nl
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/FI96-26-2.ps.gz, 19960531 Rank 2 Intersection Type Assignment in Term Rewriting Systems Steffen van Bakel Dipartimento di Informatica, Universit a degli Studi di Torino, Corso Svizzera 185, 10149 Torino, Italia bakel@di.unito.it
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/ESOP96.ps.gz, 19960531 Rewrite Systems with Abstraction and -rule: Types, Approximants and Normalization Steffen van Bakel1 Franco Barbanera2 Maribel Fern andez3 1 Department of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ, svb@doc.ic.ac.uk 2 Dipartimento di Informatica, Universit a degli Studi di Torino,
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/HOA93.ps.gz, 19960531 Strong Normalization of Typeable Rewrite Systems Steffen van Bakel1 Maribel Fern andez2 1 Afdeling Informatica, Universiteit Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, Nederland. steffen@cs.kun.nl 2 LRI B^at. 490, CNRS / Universit e de Paris-Sud, 91405 Orsay Cedex, France. maribel@lri.fr
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/RTA95.ps.gz, 19960531 (Head-)Normalization of Typeable Rewrite Systems Steffen van Bakel1 and Maribel Fern andez2 1 Dipartimento di Informatica, Universit a degli Studi di Torino, Corso Svizzera 185, 10149 Torino, Italy. bakel@di.unito.it 2 DMI - LIENS (CNRS URA 1327), Ecole Normale Sup erieure, 45, rue d'Ulm, 75005 Paris,
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/HOA95.ps.gz, 19960531 Approximation and Normalization Results for Typeable Term Rewriting Systems Steffen van Bakel and Maribel Fern andez Department of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ, svb@doc.ic.ac.uk DMI - LIENS (CNRS URA 1327) Ecole Normale Sup erieure 45 Rue d'Ulm, 75005 Paris, France
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/APAL.ps.gz, 19960531 Comparing Cubes of Typed and Type Assignment Systems Steffen van Bakel1 Luigi Liquori1 Simona Ronchi della Rocca1 Pawe Urzyczyn2y 1 Dipartimento di Informatica, Universit a degli Studi di Torino, Corso Svizzera 185, 10145 Torino, Italia. E-mail: fbakel,liquori, ronchig@di.unito.it 2 Instytut Informatyki
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/LFCS94.ps.gz, 19960531 Comparing Cubes Steffen van Bakel1 Luigi Liquori2y Simona Ronchi della Rocca2 Pawe Urzyczyn3z 1 Afdeling Informatica, Universiteit Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, Nederland. E-mail: steffen@cs.kun.nl. 2 Dipartimento di Informatica, Universit a degli Studi di Torino, Corso Svizzera 185, 10145
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/balls.ps.Z, 19960601 A Computational Model for Metric Spaces Abbas Edalat Department of Computing Imperial College 180 Queen's Gate London SW7 2BZ UK e-mail: ae@doc.ic.ac.uk Reinhold Heckmann FB 14 { Informatik Universit at des Saarlandes Postfach 151150 D-66041 Saarbr ucken, Germany e-mail: heckmann@cs.uni-sb.de January
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/async.ps, 19960603 Transforming Sequential Specifications into Concurrent and Distributed Implementations K. Lano June 3, 1996 1 Introduction This paper proposes some techniques for the transformation of abstract sequential and undistributed system specifications into concurrent and distributed implementations, and for
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/tools95.ps, 19960603
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/dp.ps, 19960603 Formalising Design Patterns K. Lano, J.C. Bicarregui1, S. Goldsack Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/vppman.ps, 19960605 ESPRIT 6500 AFRODITE VPP User Manual Authorised by: Author: Nico Plat CAP Volmac Date: January 10, 1994 Doc. ID: AFRO/CG/NP/VPPUM/V1 Afrodite in confidence Document type: Manual Status: Proposed Confidentiality: Afrodite in confidence Work Package allocation: WP-No. LT-B/T.B Distribution: Afrodite
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/jc.ps, 19960610 Development of Concurrent Systems in B AMN K. Lano , J. Dicky
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/wsecoop96.ps, 19960611 A Real-time Action Logic of Objects K. Lano, J. Bicarregui, Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ. S. Kent, Dept. of Computing, University of Brighton.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/bjdegg.ps, 19960612 Chapter 7 Integrating Formal and Structured Methods in Object-oriented System Development This chapter describes systematic approaches for the formalisation and refinement of domain and analysis models, expressed in the OMT notation of Rumbaugh , in the B Abstract Machine Notation
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/realpcfuniversal.ps.gz, 19960621 Real PCF extended with 9 is universal (Extended Abstract ) Mart n H otzel Escard o Department of Computing, Imperial College, London SW7 2BZ. Friday 21 st June 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch6-8.ps.gz, 19960627 85 Part II: Algorithms 6. Use of algorithms We now take a rest from Turing machines, and examine the use of algorithms in general practice. There are many: quicksort, mergesort, treesort, selection and insertion sort, etc., are just some of the sorting algorithms in common use, and for most problems
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/roos.ps, 19960627 Object-oriented Specification of Real-time and Reactive Systems: Case for Support 1 Previous Research Track Record Dr Lano has previously worked on the ESPRIT II REDO project, the DTI IED B User Trials project and the ESPRIT III AFRODITE project. In the B User Trials he was concerned with the
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/mediciswg.ps, 19960628 Framework 4 1994-1998 Working Group Methodology for the Development of Computer System Specifications MeDiCiS Coordinator: Kevin Lano Department of Computing, Imperial College Proposal number: 1 Summary Summary (one page) The summary should concisely address the essence of the proposal: The activities
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/CS.ps.gz, 19960628 Approximation and Normalization Results for Typeable Combinator Systems Steffen van Bakel Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, U.K. svb@doc.ic.ac.uk Maribel Fern andez DMI - LIENS, CNRS / Ecole Normale Sup erieure, 45, rue d'Ulm, 75005 Paris, France.
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/TopPLVN.ps, 19960701 1 TOPOSES POUR LES VRAIMENT NULS STEVEN VICKERS Department of Computing, Imperial College, London SW7 2BZ email sjv@doc.ic.ac.uk Restriction to geometric logic can enable one to define topological structures and continuous maps without explicit reference to topologies. This idea is illustrated with some
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/tools96.ps, 19960712 Annealing, Object Decomposition, and Design Patterns S.J. Goldsack, K. Lano Imperial College, London, England E. D urr Cap Gemini Sogeti, Netherlands July 12, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Gay/journaldraft.ps.gz, 19960712 Types for Synchronous Deadlock-Freedom Samson Abramsky Simon Gay Department of Computer Science, Department of Computer Science, University of Edinburgh Royal Holloway, University of London Rajagopal Nagarajan Department of Computing, Imperial College of Science, Technology and Medicine July 11, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/spectrum.ps.gz, 19960712 IEEE SPECTRUM 33(7), 40-43, July 1996 MOVING SOFTWARE TO A GLOBAL PLATFORM Government programs assist software firms with the goal of seeing them export $2 billion worth in the year 2000 T he present decade has already brought enormous change to the computer industry in Brazil. But the greatest change
	ftp://theory.doc.ic.ac.uk/theory/papers/DAgostino/fibtab.ps.gz, 19960719 Fibred Tableaux for Multi-Implication Logics Marcello D'Agostino and Dov M. Gabbay Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ (UK) email:fmda,dgg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/DAgostino/modalsub/grafting.ps.gz, 19960719 Grafting Modalities onto substructural implication systems Marcello D'Agostino Dov M. Gabbay Alessandra Russo Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ (UK) email:fmda,dg,ar3g@doc.ic.ac.uk 25 June 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/stat.ps.Z, 19960725 Domain of Computation of a Random Field in Statistical Physics (Extended Abstract) Abbas Edalat Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ UK.
	ftp://theory.doc.ic.ac.uk/theory/papers/vanBakel/IaC.ps.gz, 19960801 Normalization Results for Typeable Rewrite Systems STEFFEN VAN BAKEL Department of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ, U.K. E-mail: svb@doc.ic.ac.uk AND MARIBEL FERN ANDEZ DMI - LIENS (CNRS URA 1327), Ecole Normale Sup erieure, 45 rue d'Ulm, 75005 Paris, France E-mail:
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/dramwg.ps, 19960806 Proposal for ESPRIT Working Group: Distributed and ReActive system specification in Model-based languages (DRAM) 1 Project Summary This project will investigate approaches to extending the B specification language and development method with capabilities for treating concurrent, distributed or real-time
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/fusyn.ps, 19960807 A Semantic Comparison of Fusion and Syntropy K. Lano , R. Francey, J-M. Bruelz August 7, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/eugene.ps, 19960815 Real-time Action Logic and Applications K. Lano, S. Goldsack, J. Bicarregui, Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ. S. Kent, Dept. of Computing, University of Brighton.
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/BRODA/InfNDTech.ps.Z, 19960820 Pandora - A Tool for Informal Deduction using Boxproofs Krysia Broda, Susan Eisenbach and Lloyd Kamara Department of Computing, Imperial College fkb,se,ldkg@doc.ic.ac.uk 16 July 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/VPP/skkl.ps, 19960828 ESPRIT 6500 AFRODITE Axiomatic Semantics for VDM++ Authorised by: Tom Maibaum Author: Stuart Kent and Kevin Lano Date: August 28, 1996 Doc. ID: AFRO/IC/SKKL/SEM/V1 Internal Document type: Report Status: DRAFT Confidentiality: Internal Work Package allocation: Language Distribution: Afrodite Team
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/VPP/roos3.ps, 19960828 EPSRC Information and Software Technology Project No: GR/K68783 RooS RooS Semantics of RAL GR/K68783-3.003 Kevin Lano
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/cylindric5.ps.gz, 19960830 Step by Step \| Building Representations in Algebraic Logic Robin Hirsch & Ian Hodkinson
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/wollic96.ps.gz, 19960902 Axiomatising various classes of relation and cylindric algebras Robin Hirsch, Ian Hodkinson September 2, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/tvcl.ps, 19960904 Topology via Constructive Logic By STEVEN VICKERS Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's Gate, London SW7 2BZ email: s.vickers@doc.ic.ac.uk (3rd September 1996)
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/brazil.final.ps, 19960905 Real Time Formal Specification using VDM++ Eug ene D urr,1 Stephen Goldsack2 Jan van Katwijk3 1 Cap Gemini, The Netherlands 2 Imperial College, Great Britain 3 Delft University of Technology, The Netherlands
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/span.ps.gz, 19960911 Specifications as spans of geometric morphisms (Extended abstract) Till Plewe Department of Computing, Imperial College, London SW7 2BZ.
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/sobnet.ps, 19960913 Sobriety in Terms of Nets Philipp S underhauf y December 18, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/tqusnet.ps, 19960913 SMYTH COMPLETENESS IN TERMS OF NETS: THE GENERAL CASE PHILIPP S UNDERHAUF
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/tuts_q.ps.gz, 19960913 Tutorial 1: paradoxes We discuss the 'paradox' of the Pn's on pages 4-5 of the notes. Recall that P0, P1,... are all the programs of our Modula_2-like programming language, in alphabetical order. The program P was: 1 repeat forever 2 generate the next program Pn in the list 3 run Pn as far as the nth
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/compopen.ps, 19960913 On the Duality of Compact vs. Open Achim Jung University of Birmingham A.Jung@cs.bham.ac.uk Philipp S underhauf University of Southern Maine psunder@usm.maine.edu November 2, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/unifapp.ps, 19960913 Uniform Approximation of Topological Spaces Achim Jung Philipp S underhaufy January 24, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/logic.ps, 19960913 1 2 3 4 1 2 3 4 Bob Flagg Philipp S underhauf Kim Wagner A Logical Approach to Quantitative Domain Theory Preprint submitted to Elsevier Preprint 28 August 1996 flagg@usm.maine.edu psunder@usm.maine.edu Kim.Wagner@cl.cam.ac.uk Department of Mathematics and Statistics, University of Southern Maine,
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/fulob.ps, 19960913 Function Spaces for Uniformly Locally Bounded Quasi-Uniform Spaces Philipp S underhauf Fachbereich Mathematik, Arbeitsgruppe 1 Technische Hochschule Darmstadt Schlossgartenstrasse 7 D{64289 Darmstadt Germany e-mail: sunderhauf@mathematik.th-darmstadt.de February 13, 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/VdmExercises.ps, 19960919 ESPRIT 6500 AFRODITE VDM++ Exercises Using the Venus Environment Authorised by: Author: Kevin Lano (Imperial College) Nico Plat (Cap Volmac) Date: June 1995 Doc. ID: AFRO/IC/KL/VENUSEX/V3 Afrodite in confidence Document type: Standard Status: Approved Confidentiality: Afrodite in confidence Work Package
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/VDMExamples.ps, 19960919 ESPRIT 6500 AFRODITE Examples in VDM++ Authorised by: Author: N. Plat (editor) Cap Volmac Date: May 24, 1994 Doc. ID: AFRO/CG/NP/EX/V2 Afrodite in confidence Document type: Standard Status: Historic Confidentiality: Afrodite in confidence Work Package allocation: WP-No. LT-A2 Distribution: Afrodite
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/yuri.ps.gz, 19961001 Finite variable logics Ian Hodkinson Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ, England. Email: imh@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/tfm96.ps.gz, 19961003 ORDERED SOS RULES AND WEAK BISIMULATION IAIN PHILLIPS Department of Computing, Imperial College, London SW7 2BZ. IREK ULIDOWSKI Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan One of the main reasons for developing formats of rules with negative antecedents, for example the
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/drafts/actor.ps.gz, 19961005 October 5, 1996 c Carlos H. C. Duarte A Proof-Theoretic Foundation for Actor Specification and Verification Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom e-mail: cd7@doc.ic.ac.uk Actors has been regarded as a promising model for open
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/LocProd.ps.gz, 19961007 LOCALIC PRODUCTS OF SPACES TILL PLEWE
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/LocQuot.ps, 19961007 QUOTIENT MAPS OF LOCALES TILL PLEWE
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/COMBLOGICS/grafting.ps.Z, 19961008 Grafting Modalities onto substructural implication systems Marcello D'Agostino Dov M. Gabbay Alessandra Russo Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ (UK) email:fmda,dg,ar3g@doc.ic.ac.uk 25 June 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Abramsky/portfolio.ps, 19961015 Samson Abramsky January 13, 1904 Balancing the portfolio: a discussion document for he next 10 years of LFCS" Concept-oriented theory (or Eurotheory") Problem-oriented theory (or UStheory") Some time ago I led a discussion at a Lab lunch about the LFCS research themes. I was subsequently invited to
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/weakfull.ps.Z, 19961027 Math. Struct. in Comp. Science (1996), vol. 00, pp. 1{ Copyright c Cambridge University Press When Scott is Weak on the Top Abbas Edalat Department of Computing, Imperial College, 180 Queen's gate, London SW7 2BZ. ae@doc.ic.ac.uk Received received ,revised We construct an approximating chain of simple
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/TriqEff.ps.gz, 19961028 LOCALIC TRIQUOTIENT MAPS ARE EFFECTIVE DESCENT MAPS TILL PLEWE
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/AddLocQuot.ps, 19961029 ADDENDUM TO QUOTIENT MAPS OF LOCALES" TILL PLEWE
	ftp://theory.doc.ic.ac.uk/theory/papers/Dargam/thesis.ps.Z, 19961029 On Reconciling Conflicting Updates (A Compromise Revision Approach) F atima Cristina Canazaro Dargam 1996 Department of Computing Imperial College of Science, Technology and Medicine University of London This thesis is submitted to the University of London in partial fulfillment of the requirements for
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/rcats12.ps.gz, 19961101 Representability of an atomic cylindric algebra need not be determined by its atom structure Ian Hodkinson Department of Computing, Imperial College, London SW7 2BZ, UK. Draft 1.2, 1 November 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/tm-pical96.ps.gz, 19961101 Turing Machines in the Pi-Calculus Iain Phillips iccp@doc.ic.ac.uk Department of Computing Imperial College London SW7 2BZ November 1, 1996 In this brief note we show how to model Turing machines in the pi-calculus . It has long been known that TMs can be modelled in CCS and other
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/baden.ps.gz, 19961104 SYSTEM CONFIGURATION AS A MATHEMATICAL AND LOGICAL FRAMEWORK FOR ANTICIPATIVE SYSTEMS Gillian Hill Department of Computer Science, City University Northampton Square, London, EC1 4OHB E-mail: gah@cs.city.ac.uk and Department of Computing, Imperial College of Science, Technology and Medicine, 180 Queen's
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/res.ps.gz, 19961104 THE LANGUAGE OF GENERAL SYSTEMS LOGICAL THEORY: A CATEGORICAL VIEW Germano Resconi Universit a Cattolica del Sacro Cuore, Facolt a di Scienze Fisiche Matematiche e Naturali, Via Trieste 17, I{25100 Brescia, Italy email: resconi@mbox.vol.it Gillian Hill Department of Computer Science, City University and
	ftp://theory.doc.ic.ac.uk/theory/papers/Hill/wshp.ps.gz, 19961104 A CATEGORICAL WORKSPACE FOR SYSTEM CONFIGURATION GILLIAN HILL Department of Computer Science, City University Northampton Square, London, EC1V OHB and Department of Computing, Imperial College, London SW7 2BZ. System configuration describes the construction of a system from its component parts. This
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/KP.ps.gz, 19961106 GLUEING ANALYSIS FOR COMPLEMENTED SUBTOPOSES ANDERS KOCK AND TILL PLEWE
	ftp://theory.doc.ic.ac.uk/theory/papers/Broda/update5.ps, 19961108 LDS - Natural Deduction for Substructural Logics Krysia Broda , Marcelo Fingery, and Alessandra Russo email: fkb,ar3g@doc.ic.ac.uk, mfinger@ime.usp.brz November 8, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Broda/Oz.ps, 19961206 Tool Support for Informal Deduction Krysia Broda, Susan Eisenbach and Lloyd Kamara Department of Computing, Imperial College fkb,se,ldkg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Broda/Pan.ps, 19961206 Pandora - A Tool for Informal Deduction using Boxproofs Krysia Broda, Susan Eisenbach and Lloyd Kamara Department of Computing, Imperial College fkb,se,ldkg@doc.ic.ac.uk 6 December 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/biquotients.ps.gz, 19961210 Induction and recursion on the partial real line via biquotients of bifree algebras Mart n H otzel Escard o m.escardo@doc.ic.ac.uk Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom Thomas Streicher streicher@mathematik.th-darmstadt.de Fachbereich Mathematik,
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/rcats13.ps.gz, 19961212 Representability of an atomic cylindric algebra need not be determined by its atom structure Ian Hodkinson Department of Computing, Imperial College, London SW7 2BZ, UK. Draft 1.3, 11 December 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Vickers/TopCat.ps, 19961216 TOPICAL CATEGORIES OF DOMAINS DRAFT OF December 16, 1996. Steven Vickers, Department of Computing, Imperial College, 180 Queen s Gate, London, SW7 2BZ. email: sjv@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Broda/TrMeLDS.ps, 19961218 TRANSFORMATION METHODS IN LDS K. BRODA, M. D'AGOSTINO AND A. RUSSO Department of Computing Imperial College of Science, Technology and Medicine 180, Queen's Gate, London SW7 2BZ kb,mda,ar3@doc.ic.ac.uk 1. Introduction The methodology of Labelled Deductive Systems\| or simply LDS1\| is a unifying framework
	ftp://theory.doc.ic.ac.uk/theory/papers/McCusker/thesis.ps.gz, 19961220 University of London Imperial College of Science, Technology and Medicine Department of Computing Games and Full Abstraction for a Functional Metalanguage with Recursive Types Guy Andrew McCusker A thesis submitted for the degree of Doctor of Philosophy of the University of London and for the Diploma of
	ftp://theory.doc.ic.ac.uk/theory/papers/McCusker/fpcfull.ps.gz, 19961220 Games and Full Abstraction for FPC Guy McCusker St. John's College, Oxford, United Kingdom OX1 3JP. email: mccusker@comlab.ox.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/arturo.ps, 19970115 EPSRC Information and Software Technology Project No: GR/K68783 RooS RooS Specification of a Chemical Process Controller in VDM++ and B GR/K68783-11.003 Kevin Lano, Arturo Sanchez
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/WOLLIC/lastversion2.ps.Z, 19970116 LDS-Natural Deduction for Substructural Logics Krysia Broda , Marcelo Fingery, and Alessandra Russo email: fkb,ar3g@doc.ic.ac.uk, mfinger@ime.usp.brz December 18, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/coord.ps.Z, 19970122 ESPRIT BR Project 9102 { COORDINATION Final Report Chris Hankin (ed) 1 Introduction The Coordination project was funded under the LTR programme. The intial contract was for 24 months starting in February 1994; subsequently, the project was granted a 3 month no-cost extension. The partners were Imperial
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/sem1.ps.Z, 19970122 ESPRIT Basic Research Action 3124 - Semantique Final Report edited by Chris Hankin Dept. of Computing, Imperial College 180 Queen's Gate, LONDON SW7 2BZ, UK e-mail: clh@doc.ic.ac.uk 1 Executive Summary 1.1 Overview Despite over thirty years of development, software engineering" is still fundamentally a
	ftp://theory.doc.ic.ac.uk/theory/papers/Hankin/sem2.ps.Z, 19970122 ESPRIT WG 6809 - Semantique 2 Final Report Chris Hankin (editor) 1 Introduction This document is the final report for Working Group 6809 - Semantique 2. The group was funded from 25th July 1992 until 24th October 1995 (including a 3 month no-cost extension). The partners in the group are DAIMI(Aarhus,
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/vdmpp_rt.ps, 19970124 Integrating VDM++ and Real-time System Design K. Lano, S. Goldsack, J. Bicarregui, Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ. S. Kent, Dept. of Computing, University of Brighton.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/arts_tank.ps, 19970124 Transformational Formal Development of Real-time Systems K. Lano, Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ. A. Sanchez, Centre for Process Systems Engineering, Imperial College.
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/apal.ps.gz, 19970131 Atom structures of cylindric algebras and relation algebras Ian Hodkinson Department of Computing, Imperial College, London SW7 2BZ, UK. email imh@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/cr.ps.gz, 19970131 Complete Representations in Algebraic Logic Robin Hirsch & Ian Hodkinson
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/eicqf.ps, 19970201 The essence of ideal completion in quantitative form Robert C. Flagg 1 Philipp S underhauf 2;3 Department of Mathematics and Statistics, University of Southern Maine, Portland ME 04104-9300, USA If a posets lacks joins of directed subsets, one can pass to its ideal completion. But doing this means also
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Mackie/bibliography.ps, 19970203 BIBLIOGRAPHY (Abramsky, 1993) Samson Abramsky. Computational Interpretations of Linear Logic. Journal of Theoretical Computer Science, 111(1):3 57, 1993. (Andreoli and Pareschi, 1991) Jean-Marc Andreoli and Remo Pareschi. Linear objects: Logical processes with built-in inheritance. New Generation
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Mackie/final.ps, 19970203 CONTENTS LIST OF FIGURES xi FOREWORD xiii PREFACE xv ACKNOWLEDGEMENTS xvii CHAPTER 1 INTRODUCTION 1 1 OVERVIEW : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 6 CHAPTER 2 CLASSICAL PROPOSITIONAL LOGIC 11 1 SYNTAX : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 11 2 SEMANTICS :
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/arts_tank.ps, 19970204 Transformational Formal Development of Real-time Systems K. Lano, Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ. A. Sanchez, Centre for Process Systems Engineering, Imperial College.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/zum_paper.ps, 19970204 Specifying Reactive Systems in B AMN K. Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/arts_c2d.ps, 19970204 Specification and Refinement of Continuous Real-time Systems Stephen Goldsack, Kevin Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ, UK Eugene Durr CAP Volmac, Dolderseweg 2, 3712 BP Huis ter Heide, The Netherlands
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/fme_paper.ps, 19970204 Design of Real-time Control Systems for Event-driven Operations K. Lano , A. Sanchez
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/arts_c2d.ps, 19970204 Specification and Refinement of Continuous Real-time Systems Stephen Goldsack, Kevin Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ, UK Eugene Durr CAP Volmac, Dolderseweg 2, 3712 BP Huis ter Heide, The Netherlands
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/bconf_paper.ps, 19970204 Using B to Design and Verify Controllers for Chemical Processing K. Lano, J. Bicarregui , A. Sanchez
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/drafts/transact.ps.gz, 19970204 September, 1996 c Carlos H. C. Duarte On the use of Transactions to Modularise Formal Specifications Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom E-mail: cd7@doc.ic.ac.uk 1 Introduction The use of transactions as a means of structuring
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/tutorial.ps, 19970204 ESPRIT 6500 AFRODITE The Development of Concurrent and Real-time Systems using VDM++ Authorised by: Author: Eug ene D urr (Cap Volmac) Stephen Goldsack (Imperial College) Date: June 1995 Doc. ID: AFRO/CG/ED/COURSE/V1 Public Document type: Standard Status: Approved Confidentiality: Public Work Package
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/acid.ps.gz, 19970204 Special Issues in Object-Oriented Programming, Max M uhlh auser (editor), Dpunkt Verlag, 1996. Acidity Yields Another Notion for Modularity in Formal Object-Oriented Specifications1 Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom e-mail:
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Mackie/newprelims.ps, 19970220 EDITORIAL PREFACE The last twenty years have witnessed an accelerated development of pure and applied logic, particularly in response to the urgent needs of computer science. Many traditional logicians have developed interest in applications and in parallel a new generation of researchers in logic has
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Mackie/3March-Mackie.ps, 19970303 EDITORIAL PREFACE The last twenty years have witnessed an accelerated development of pure and applied logic, particularly in response to the urgent needs of computer science. Many traditional logicians have developed interest in applications and in parallel a new generation of researchers in logic has
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/tapsoft97.ps.gz, 19970313 Formats of Ordered SOS Rules with Silent Actions Irek Ulidowski1 and Iain Phillips2 1 Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan 2 School of Computing, Imperial College, London, England
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/ordered97.ps.gz, 19970313 Formats of Ordered SOS Rules with Silent Actions Irek Ulidowski Research Institute for Mathematical Sciences, Kyoto University, Kitashirakawa, Sakyo-ku, Kyoto 606-01, Japan email: irek@kurims.kyoto-u.ac.jp Iain Phillips Department of Computing, Imperial College,180 Queen's Gate, London SW7 2BZ, United
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Brink/psps.ps, 19970317 Power Structures and Program Semantics by Chris Brink and Ingrid Rewitzky 31 January 1997 CONTENTS PREFACE iv CHAPTER 1 THE PARADIGM TRIANGLE 1 1.1 DECLARING THE PARADIGM : : : : : : : : : : : : : : : : : : 1 1.2 CLASSICAL PROPOSITIONAL LOGIC : : : : : : : : : : : : : 4 1.3 MODAL LOGIC : : : : : : : : :
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/well.ps, 19970402 Smyth Completion as Bicompletion Ralph Kopperman Department of Mathematics City College of New York rdkcc@cunyvm.cuny.edu Philipp S underhauf y Department of Computing Imperial College London P.Sunderhauf@doc.ic.ac.uk Bob Flagg Department of Mathematics and Statistics University of Southern Maine
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/mcat.ps, 19970408 EPSRC Information and Software Technology Project No: GR/K68783 RooS RooS Refinement and Simulation of Real-time and Hybrid Systems using VDM++ and gPROMS GR/K68783-13.003 Kevin Lano
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Ohlbach/book.ps, 19970410 Logic, Language and Reasoning Essays in Honor of Dov Gabbay, Part I edited by Uwe Reyle and Hans J urgen Ohlbach 1 2 Preface This volume is dedicated to Dov Gabbay who celebrated his 50th birthday in October 1995. Dov is one of the most outstanding amd most productive researchers we have ever met. He
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/ecooprt97.ps, 19970411 Formalising Real-time System Design K. Lano, S. Goldsack Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ.
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/thesis.ps.gz, 19970425 University of London Imperial College of Science, Technology and Medicine Department of Computing PCF extended with real numbers: a domain-theoretic approach to higher-order exact real number computation Mart n H otzel Escard o Dr. Michael B. Smyth Supervisor Prof. Achim Jung External Examiner Prof.
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/lics97b.ps.gz, 19970425 Semantics of Exact Real Arithmetic Peter John Potts Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fpjp,ae,mheg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/fullintegrationpcf.ps.gz, 19970425 Integration in Real PCF Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, UK fae,mheg@doc.ic.ac.uk Wednesday 11 th December 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/449.ps, 19970513 Specification of Required Non-determinism J Fiadeiro, A Lopes Dept. of Informatics, University of Lisbon, Campo Grande, 1700 Lisbon. K Lano, J Bicarregui Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/planv2.ps, 19970518 40' Door Door Door (10') (10') (10') 60' Stage (10'6') T T T T T TT R R R R R R T T Trestle table: 6'3' Round table: 1.5m diameter R (6) (8)Chair: 2'1.5' (40) Stage is 15 of 2'2' staging blocks or equivalent: 10'*6'
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/planv1.ps, 19970518 40' Door Door Door (10') (10') (10') 60' Stage (10'6') T T T T T TT R R R R R R T T Trestle table: 6'3' Round table: 1.5m diameter R (6) (8)Chair: 2'1.5' (40) Stage is 15 of 2'2' staging blocks or equivalent: 10'*6'
	ftp://theory.doc.ic.ac.uk/theory/papers/DAgostino/grafting.ps.gz, 19970520 Grafting Modalities onto substructural implication systems Marcello D'Agostino Dov M. Gabbay Alessandra Russo Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ (UK) email:fmda,dg,ar3g@doc.ic.ac.uk 25 June 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/newrep.ps.Z, 19970521 Electronic Notes in Theoretical Computer Science 6 (1997) URL: http://www.elsevier.nl/locate/entcs/volume6.html 14 pages A New Representation for Exact Real Numbers 1 Abbas Edalat Peter John Potts Department of Computing Imperial College of Science, Technology, and Medicine London SW7 2BZ, England E. N.
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/realsemantics.ps.gz, 19970525 Semantics of Exact Real Arithmetic Peter John Potts Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fpjp,ae,mheg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/computerarithmetic.ps.gz, 19970525 Exact Real Computer Arithmetic Peter John Potts Abbas Edalat Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom fpjp,aeg@doc.ic.ac.uk 21 March 1997 1 Introduction Real numbers are usually represented by finite strings of digits belonging to some digit set. The real
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/realalgorithms.ps.gz, 19970525 Exact Real Arithmetic based on Linear Fractional Transformations Peter John Potts Abbas Edalat Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom fpjp,aeg@doc.ic.ac.uk 1 December 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/fme2.ps, 19970529 Specification of Required Non-determinism J Fiadeiro, A Lopes Dept. of Informatics, University of Lisbon, Campo Grande, 1700 Lisbon. K Lano, J Bicarregui Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/ifm.ps, 19970530 A FORMAL APPROACH TO DESIGN PATTERNS IN RE-ENGINEERING N. Malik, K. Lano Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ, UK
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/tacs97.ps, 19970602 A Type-theoretic Approach to Deadlock-freedom of Asynchronous Systems Samson Abramsky1, Simon Gay2, and Rajagopal Nagarajan3 1 Department of Computer Science, University of Edinburgh, Mayfield Road, Edinburgh, UK, EH9 3JZ; samson@dcs.ed.ac.uk 2 Department of Computer Science, Royal Holloway, University
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/RefUCRI.ps, 19970609 Notes on Refinement, Interpolation and Uniformity T. Dimitrakos and T.S.E. Maibaum Department of Computing, Imperial College, London SW7 2BZ ftd, tsemg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/UcriInDWS.ps, 19970609 Uniform interpolation in a Development Workspace. Theodosis Dimitrakos Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ td@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/CriRef.ps, 19970609 On the role of interpolation in stepwise refinement. T. Dimitrakos and T.S.E. Maibaum Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ ftd,tsemg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Russo/Napoli/Mathware-paper.ps.Z, 19970611 66 Mathware & Soft Computing 3 (1996) 67-82 Information Frames, Implication Systems and Modalities Marcello D'Agostino, Dov M. Gabbay, Alessandra Russo Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ (UK) email:fmda,dg,ar3g@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/lbfl_fme97.ps, 19970615 Specification of Required Non-determinism K Lano, J Bicarregui Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ J Fiadeiro, A Lopes Dept. of Informatics, University of Lisbon, Campo Grande, 1700 Lisbon.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/lasa_fme97.ps, 19970615 Design of Reactive Control Systems for Event-driven Operations K. Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ A. Sanchez Centre for Process Systems Engineering, Imperial College, London SW7 2BY. Current address: Departmento de Ingenieria Electrica. CINVESTAV-Gdl. Apdo.
	ftp://theory.doc.ic.ac.uk/theory/papers/Nagarajan/tcs_draft.ps, 19970618 Types for Deadlock-freedom: The Synchronous Case Samson Abramsky Simon Gay Department of Computer Science, Department of Computer Science, University of Edinburgh, Royal Holloway, Mayfield Road, University of London, Edinburgh EH9 3JZ, UK. Egham, Surrey TW20 0EX, UK. samson@dcs.ed.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/steam_boiler_oc_b.ps, 19970618 From Temporal Logic Specifications to B Implementations: Development of the Steam Boiler K. Lano, J. Bicarregui, T. Maibaum Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ kcl@doc.ic.ac.uk June 18, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/fullinduction.ps.gz, 19970619 Induction and recursion on the partial real line with applications to Real PCF Mart n H otzel Escard o Thomas Streichery Thursday 19 th June 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/zu-wsroot.ps, 19970626 Invariants as Design Templates in Object-based Systems S.J. Goldsack, K. Lano Imperial College, London, England E. D urr Cap Gemini Sogeti, Netherlands
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/zu-ws.ps, 19970708 Invariants as Design Templates in Object-based Systems S.J. Goldsack, K. Lano, Department of Computing Imperial College of Science, Technology and Medicine, 180 Queens Gate, London SW7 2BZ, England Tel (+44) 171 594 8246 email sjg@doc.ic.ac.uk email kcl@doc.ic.ac.uk E. D urr Utrecht University Dept.
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/toolspacific.ps, 19970708 Annealing, Object Decomposition, and Design Patterns. S.J. Goldsack, K. Lano Imperial College, London, England E. D urr Cap Gemini, Netherlands
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/nf.ps, 19970709 Design of Reactive Control Systems for Event-driven Operations K. Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ A. Sanchez Centre for Process Systems Engineering, Imperial College, London SW7 2BY. Current address: Departmento de Ingenieria Electrica. CINVESTAV-Gdl. Apdo.
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/CLNA.ps.gz, 19970710 Math. Struct. in Comp. Science (1993), vol. 11, pp. 1{000 Copyright c Cambridge University Press Categorical logic of names and abstraction in action calculi Du <=s ko Pav l ov i cy COGS, University of Sussex, Brighton, UK e-mail: duskop@cogs.susx.ac.uk Received Milner's action calculus implements
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/CCPS2.ps.gz, 19970710 Convenient categories of asynchronous processes and simulations Du<=sko Pavlovi c COGS, University of Sussex, Brighton, England; e-mail: duskop@cogs.susx.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/s97.ps, 19970710 Reengineering Legacy Applications using Design Patterns K. Lano Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ Email: kcl@doc.ic.ac.uk N. Malik Systems (Private) Limited, Karachi, Pakistan
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/4c.ps.gz, 19970710 A categorical setting for the 4-Colour Theorem Du<=sko Pavlovi c Department of Mathematics and Statistics, McGill University Montreal, Quebec, Canada
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/chuI.ps.gz, 19970710 Math. Struct. in Comp. Science (1993), vol. 11, pp. 1{000 Copyright c Cambridge University Press Chu I: cofree equivalences, dualities and -autonomous categories Du<=sko Pavlovi cy Department of Computing, Imperial College, London SW7 2BZ, UK Received We study three comonads derived from the comma
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/mapsII.ps.gz, 19970710 Maps II: Chasing diagrams in categorical proof theory Du<=sko Pavlovi c Dedicated to Jim Lambek in friendship and admiration
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/SIC.ps.gz, 19970710 Specifying Interaction Categories D. Pavlovi c and S. Abramskyy
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/CCPS1.ps.gz, 19970710 Convenient Category of Processes and Simulations I: Modulo Strong Bisimilarity Du<=sko Pavlovi c
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/CLCI.ps.gz, 19970710 CATEGORICAL LOGIC OF CONCURRENCY AND INTERACTION. I: SYNCHRONOUS PROCESSES DU<=SKO PAVLOVI C Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom E-mail: D.Pavlovic@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Pavlovic/draft.ps.gz, 19970711 Process categories as fixed points or: Typed processes, timed computations (Working draft) S. Abramsky and D. Pavlovi cy June 27, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/fcbs.ps, 19970711 Composition of Reactive System Components K. Lano, J. Bicarregui, T. Maibaum Dept. of Computing, Imperial College, 180 Queens Gate, London SW7 2BZ kcl@doc.ic.ac.uk J. Fiadeiro Dept. of Informatics, University of Lisbon, Campo Grande, 1700 Lisbon July 11, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/EdalatHeckmann.ps.Z, 19970715 A Computational Model for Metric Spaces Abbas Edalat Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ UK Reinhold Heckmann FB 14 { Informatik, Universit at des Saarlandes, Postfach 151150, D-66041 Saarbr ucken, Germany
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/waybelow.ps.gz, 19970722 The way-below relation of function spaces over semantic domains Thomas Erker Mart n H otzel Escard oy Klaus Keimel To appear in Topology and Its Applications Version of Tuesday 22 nd July 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/ahn.ps.gz, 19970731 Finite algebras of relations are representable on finite sets H. Andr eka, I. Hodkinson, I. N emeti 25 June 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Plewe/PPT.ps.gz, 19970811 Mathematik{Arbeitspapiere Universit at Bremen, 1997 Regular monomorphisms of Hausdorff frames T. Plewe A. Pultry A. Tozzi In honour of Horst Herrlich on the occassion of his 60th birthday.
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/summary_cc96.ps.gz, 19970903 In P. Fritzon (ed), Poster Proc. CC'96 - Int. Conf. Compiler Construction, TR 96-12, Comp. Dept., Linkoping Univ., 49-56, 1996. On the Systematic Development of Compilers: A Case Study Carlos H. C. Duarte Roberto Ierusalimschy Department of Computing Departamento de Inform atica Imperial College, London
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/resumo.ps.gz, 19970903 Em Anais PANEL'95 - XXI Confer^encia Latino-Americana em Inform atica, 743{754. Julho/Agosto, 1995. Aplicando um m etodo orientado a objetos para desenvolvimento de compiladores Carlos H. C. Duarte Roberto Ierusalimschy Department of Computing Departamento de Inform atica Imperial College, London PUC,
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/NegationPrelims.ps, 19970909 CONTENTS PREFACE xi PART I MODELS, RELEVANCE AND IMPOSSIBILITY 1 ARNON AVRON Negation: Two Points of View 3 J. MICHAEL DUNN A Comparative Study of Various Model-theoretic Treatments of Negation: A History of Formal Negation 23 GREG RESTALL Negation in Relevant Logics (How I stopped worrying and learned
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Look.ps, 19970909 Another Look at Generalised Quantifiers D. M. Gabbay 1st Draft August 1996 2nd Draft September 1996 Expanded 2nd Draft September 1996 3rd Draft July 1997 1 Introduction and Motivation This paper is a modest addition to van Lambalgen's theory of generalised quantifiers. We introducea generalised
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Products.ps, 19970915 PRODUCTS OF MODAL LOGICS Dov Gabbay Department of Computing Imperial Collage 180 Queen's Gate London SW7 2BZ UK Valentin Shehtman Institute for Problems of Information Transmission Russian Academy of Sciences B. Karetny 19 101447, Moscow Russia Preliminary version July 1997 Contents 1 Introduction and
	ftp://theory.doc.ic.ac.uk/theory/papers/Webster/tesi.ps, 19970916 University of London Imperial College of Science, Technology and Medicine Department of Computing Topology and measure theory in the digital setting: on the approximation of spaces by inverse sequences of graphs Julian Webster A thesis submitted for the degree of Doctor of Philosophy of the University
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/injective.ps.gz, 19970922 Properly injective spaces and function spaces Mart n H otzel Escard o To appear in Topology and Its Applications Version of Monday 22 nd September 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/JLogComp/V7_5.ps, 19970925 Journal of Logic and Computation Contents Original Articles 555Deterministic and Non-deterministic Stable Models D. Sacc a and C. Zaniolo 581Functional Translation and Second-Order Frame Properties of Modal Logics H. J. Ohlbach and R. A. Schmidt 605Beyond Rational Monotony: Some Strong Non-Horn Rules
	ftp://theory.doc.ic.ac.uk/theory/papers/Malacaria/cc.ps, 19971006 A New Approach to Control Flow Analysis Pasquale Malacaria Chris Hankin Dept. of Computing Imperial College LONDON SW7 2BZ pm5,clh@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/survey.ps.Z, 19971013 Domains for Computation in Mathematics, Physics and Exact Real Arithmetic Abbas Edalat Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ UK ae@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/efficient.ps.gz, 19971021 Efficient on-line computation of real functions using exact floating point Peter John Potts Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK 17 October 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/tensors.ps.gz, 19971021 A note on tensors in the LFT approach to exact real arithmetic Philipp S underhauf Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ United Kingdom p.sunderhauf@doc.ic.ac.uk October 21, 1997 1 Introduction One approach to exact real number arithmetic is based on linear
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/other/buzz.ps.gz, 19971022 Greetings. I am Peter Potts. I come in peace. 1 Stand back everyone. To infinity and beyond. 2 Nirvana is coming. The mystery portal awaits. 3
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/letter2.ps.gz, 19971022 Mr. P. J. Potts Huxley Building Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Email: pjp@doc.ic.ac.uk 15 May 1996 Prof. Dr. F. H. Busse Coordinating Editor of Physica D Physikalisches Institut Universit at Bayreuth 95440
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part1/domain.ps.gz, 19971022 FAIT 2.5 Domain Theory Dr. Abbas Edalat Extended Coursework Domain Equations Peter John Potts 24 March 1995 1 Introduction Most programming languages allow recursive definitions in which the name of the entity being defined can "recur" in its own definition. The mathematical theory known as "domain
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/examples/database.ps.gz, 19971022 Example of Bibliographic Database Peter John Potts December 15, 1995 1 Indroduction Here is just a FEW citations
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/draft.ps.gz, 19971022 Computable Real Arithmetic Using Linear Fractional Transformations Peter John Potts Huxley Building Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ Telephone number: 0171 594 8241 Fax number: 0171 581 8024 E-mail address: P.Potts@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/stanford.ps.gz, 19971022 Exact Real Arithmetic based on Linear Fractional Transformations Peter John Potts Abbas Edalat Department of Computing Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom fpjp,aeg@doc.ic.ac.uk 1 December 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/edge/lecture.ps.gz, 19971022 A Smooth Approximation on the Edge of Chaos by Peter John Potts http://theory.doc.ic.ac.uk/~pjp and supervised by Abbas Edalat Imperial College of Science, Technology and Medicine 1 Overview Last talk entitled "The Storage Capacity of Forgetful Neural Networks". I described a two stage algorithm to
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/lics/submission.ps.gz, 19971022 Semantics of Exact Real Arithmetic Peter John Potts Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fpjp,ae,mheg@doc.ic.ac.uk 1. Introduction It is generally accepted that floating-point computation is suitable for a wide range of
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/examples/sprocl.ps.gz, 19971022 INSTRUCTIONS FOR PRODUCING A CAMERA-READY MANUSCRIPT USING IMPERIAL COLLEGE PRESS STYLE FILES A.B. AUTHOR, C.D. AUTHOR Imperial College Press Co, Room 516, Sherfield Building Imperial College, London SW7 2AZ, UK A.N. OTHER Department of Computing, Imperial College, London SW7 2BZ. This is where the
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/other/unix.ps.gz, 19971022 The UNIX Operating System Peter John Potts March 6, 1996
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/submission2.ps.gz, 19971022 The Storage Capacity of Forgetful Neural Networks ffl Corresponding Author Peter John Potts Room 563b Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Telephone number: 0171 594 8241 Fax number: 0171 581 8024 E-mail address:
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/letter3.ps.gz, 19971022 Mr. P. J. Potts Huxley Building Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Email: pjp@doc.ic.ac.uk 11 July 1996 Prof. Dr. F. H. Busse Coordinating Editor of Physica D Physikalisches Institut Universit at Bayreuth 95440
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/rebuttal.ps.gz, 19971022 Mr. P. J. Potts Huxley Building Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Email: pjp@doc.ic.ac.uk 11 July 1996 First Referee for Physica D Physikalisches Institut Universit at Bayreuth 95440 Bayreuth Germany Dear
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/examples/index.ps.gz, 19971022 Example of Make Index Peter John Potts December 6, 1995 Chapter 1 Indroduction The lion is the king of the jungle. However, the cheetah is the fastest animal in the world. 1 A parate may be beautifully coloured, but talk about useless. The eagle is much more interesting. 2 Index cheetah, 1 eagle, 2
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/lecture.ps.gz, 19971022 The Storage Capacity of Forgetful Neural Networks Talk based on MSc Thesis by Peter John Potts and supervised by Abbas Edalat Imperial College of Science, Technology and Medicine 1 Overview In this talk, we will derive a two stage algorithm to evaluate the storage capacity of a forgetful neural network
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/submission3.ps.gz, 19971022 The Storage Capacity of Forgetful Neural Networks ffl Corresponding Author Peter John Potts Room 563b Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Telephone number: 0171 594 8241 Fax number: 0171 581 8024 E-mail address:
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/other/cv.ps.gz, 19971022 Curriculum Vitae Peter John Potts Personal Peter John Potts, born 14 May 1966, male, British, single. 36a Douglas Road, Canonbury, London N1 2LD, UK, +44 (0)956 665074 Education Date Institution Qualification Subject Grade Oct 95 Imperial College PhD Computer Science to London University (Exact Real Sep
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/lics/paper.ps.gz, 19971022 Semantics of Exact Real Arithmetic Peter John Potts Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fpjp,ae,mheg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/thesis.ps.gz, 19971022 Imperial College of Science, Technology and Medicine (University of London) Department of Computing
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/real.ps.Z, 19971022 A domain-theoretic approach to computability on the real line 1 Abbas Edalat and Philipp S underhauf Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ United Kingdom fae,ps15g@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/letter4.ps.gz, 19971022 Mr. P. J. Potts Huxley Building Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Email: pjp@doc.ic.ac.uk 8 October 1996 Prof. Dr. F. H. Busse Coordinating Editor of Physica D Physikalisches Institut Universit at Bayreuth 95440
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/comprox/lecture.ps.gz, 19971022 Computable Real Arithmetic using Linear Fractional Transformations by Peter John Potts http://theory.doc.ic.ac.uk/~pjp and supervised by Abbas Edalat Imperial College of Science, Technology and Medicine 1
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/edge/paper.ps.gz, 19971022 A SMOOTH APPROXIMATION ON THE EDGE OF CHAOS P. J. POTTS Department of Computing, Imperial College, London SW7 2BZ. It is known that for almost all starting points the non-deterministic dynamical system corresponding to a hyperbolic iterated function system with probabilities generates orbits whose
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/submission.ps.gz, 19971022 The Storage Capacity of Forgetful Neural Networks ffl Corresponding Author Peter John Potts Room 563b Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom Telephone number: 0171 594 8241 Fax number: 0171 581 8024 E-mail address:
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/pamphlet.ps.gz, 19971022 The Storage Capacity of Forgetful Neural Networks Peter John Potts Based on Msc thesis supervised by Abbas Edalat Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ September 1995
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/msc/part2/physicad/letter.ps.gz, 19971022 Mr. P. J. Potts Huxley Building Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ United Kingdom 8 January 1996 Prof. Dr. F. H. Busse Coordinating Editor of Physica D Physikalisches Institut Universit at Bayreuth 95440 Bayreuth Germany Dear
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/normal.ps.gz, 19971022 Exact Real Computer Arithmetic Peter John Potts Abbas Edalat Departmental Technical Report DOC 97/9 Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom fpjp,aeg@doc.ic.ac.uk 21 March 1997 1 Introduction Real numbers are usually represented by finite strings of digits belonging to some
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/mfps/abstract.ps.gz, 19971022 Electronic Notes in Theoretical Computer Science 6 (1997) URL: http://www.elsevier.nl/locate/entcs/volume6.html 13 pages A New Representation for Exact Real Numbers 1 Abbas Edalat Peter John Potts Department of Computing Imperial College of Science, Technology, and Medicine London SW7 2BZ, England E. N.
	ftp://theory.doc.ic.ac.uk/theory/papers/Potts/phd/ieee.ps.gz, 19971022 Efficient on-line computation of real functions using exact floating point Peter John Potts Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK 17 October 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/DWS.ps, 19971024 Development Workspaces: an introduction T. Dimitrakos and T.S.E. Maibaum Department of Computing, Imperial College, London SW7 2BZ ftd, tsemg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/ASE97.ps, 19971024 Notes on Refinement, Interpolation and Uniformity. T. Dimitrakos and T.S.E. Maibaum Department of Computing, Imperial College, London SW7 2BZ ftd, tsemg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/ndimbases.ps.gz, 19971024 Relation algebras with n-dimensional relational bases Draft version 3.1 Robin Hirsch and Ian Hodkinson October 24, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Dimitrakos/UIMS.ps, 19971024 Uniformity, Interpolation and Module specification in a Development Workspace T. Dimitrakos and T.S.E. Maibaum Imperial College, 180 Queen's Gate, London SW7 2BZ, U.K.
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/qmetric.ps, 19971031 Spaces of valuations as quasimetric domains Philipp S underhauf Department of Computing Imperial College London SW7 2BZ P.Sunderhauf@doc.ic.ac.uk October 31, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/sk.ps, 19971031 Refinement through Pictures: Formalising Syntropy Refinement Concepts K. Lano, J. Bicarregui Dept. of Computing, Imperial College, 180 Queens Gate, London, SW7 2BZ October 31, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/actor-modelage.ps.gz, 19971103 In P.-Y. Schobbens and A. Cesta (eds), Formal Models of Agents - Proc. Esprit WS ModelAge, 115-128, 1997. Towards a Proof-Theoretic Foundation for Actor Specification and Verification Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom e-mail:
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/papers/location.ps.gz, 19971103 H. Bowman and J. Derrick (eds), Proc. 2nd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems, 1997. A proof-theoretic approach to the design of object-based mobility Carlos H. C. Duarte Department of Computing, Imperial College 180 Queen's Gate, London, SW7 2BZ, United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Escardo/papers/top97.ps.gz, 19971103 Injective spaces and the filter monad Mart n H otzel Escard o Department of Computing, Edinburgh University Version of Monday 3 rd November 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/reals.ps, 19971104 A domain-theoretic approach to computability on the real line 1 Abbas Edalat and Philipp S underhauf Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ United Kingdom fae,ps15g@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/DRUMS/Volume1/Volume1.ps, 19971111 CONTENTS PREFACE vii PHILIPPE SMETS Probability, Possibility, Belief: Which and Where 1 GIOVANNI PANTI Multi-valued Logics 25 VIL EM NOV AK Fuzzy Logic 75 COLIN HOWSON The Bayesian Approach 111 DONALD GILLIES Confirmation Theory 135 DIDIER DUBOIS AND HENRI PRADE Possibility Theory: Qualitative and
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Hansson/Main.ps, 19971125 CONTENTS PREFACE xi SUGGESTED COURSES 1 CHAPTER 1 HAVING BELIEFS 3 1 WHAT IS BELIEF DYNAMICS : : : : : : : : : : : : : : : : : : : 3 2 ANSWER MODES AND DOXASTIC ATTITUDES : : : : : : : : : 4 3 INPUTS : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 4 BELIEF STATES AND BELIEF SETS : : :
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/apchp.ps, 19971126 K. Lano, S. Goldsack, A. Sanchez 1 Formal Development of Event-Driven Controllers for Process Manufacturing Systems 1.1 Introduction This chapter shows the combined use of formal methods with techniques developed in control engineering for the design and development of automation systems for
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/COOTS.ps, 19971208 Design Patterns and their Role in Formal Object-oriented Development Kevin Lano, Stephen Goldsack December 8, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/logicbisim.ps.Z, 19971210 A Logical Characterization of Bisimulation for Labeled Markov Processes Jos ee Desharnais School of Computer Science McGill University Montreal, Quebec, Canada desharna@cs.mcgill.ca Abbas Edalaty Department of Computing Imperial College London, UK ae@doc.ic.ac.uk Prakash Panangadenz School of Computer
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/doc-only/sigma93.ps.gz, 19971212 DRAFT CCS with Broadcast Stability Iain Phillips Department of Computing Imperial College of Science, Technology and Medicine January 17, 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/expr93.ps.gz, 19971212 A Note on Expressiveness of Process Algebra Iain Phillips iccp@doc.ic.ac.uk Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ, United Kingdom
	ftp://theory.doc.ic.ac.uk/theory/papers/Phillips/doc-only/priority94.ps.gz, 19971212 Approaches to priority in process algebra Iain Phillipsy iccp@doc.ic.ac.uk Department of Computing Imperial College London SW7 2BZ August 15, 1994
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/banach.ps, 19971215 Computable Banach Spaces via Domain Theory 1 Abbas Edalat and Philipp S underhauf Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ United Kingdom fae,ps15g@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/lcrf.ps.gz, 19971216 Lazy Computation with Exact Real Numbers Abbas Edalat Peter John Potts Philipp S underhauf Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fa.edalat,p.potts,p.sunderhaufg@doc.ic.ac.uk 16th December 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/Hansson/Hansson.ps, 19971216 CONTENTS PREFACE xi SUGGESTED COURSES 1 CHAPTER 1 HAVING BELIEFS 3 1 WHAT IS BELIEF DYNAMICS : : : : : : : : : : : : : : : : : : : 3 2 ANSWER MODES AND DOXASTIC ATTITUDES : : : : : : : : : 4 3 INPUTS : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 7 4 BELIEF STATES AND BELIEF SETS : : :
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/lcrf.ps, 19971216 Lazy Computation with Exact Real Numbers Abbas Edalat Peter John Potts Philipp S underhauf Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fa.edalat,p.potts,p.sunderhaufg@doc.ic.ac.uk 16th December 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/banach.ps.gz, 19971216 Computable Banach Spaces via Domain Theory 1 Abbas Edalat and Philipp S underhauf Department of Computing, Imperial College 180 Queen's Gate, London SW7 2BZ United Kingdom fae,ps15g@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Sunderhauf/incr.ps, 19980102 Incremental Addition in Exact Real Arithmetic Philipp S underhaufy December 31, 1997
	ftp://theory.doc.ic.ac.uk/theory/papers/Goldsack/wp2.ps, 19980120 Object Reification in VDM++ Stephen J. Goldsack Imperial College of Science, Technology and Medicine,London Eug ene D urr, Nico Plat Cap Volmac, 3712 BP Huis ter Heide, The Netherlands
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/misc/curric1.ps.gz, 19980120 Curriculum Vitae Resumido Carlos Henrique Cabral Duarte 20 de Janeiro de 1998 Curriculum Vitae Resumido - Carlos H. C. Duarte 1 1 - Identifica c~ao 1. Nome: Carlos Henrique Cabral Duarte 2. Data de nascimento: 01/07/1970 3. Naturalidade: Juiz de Fora, MG 4. Nacionalidade: Brasileira 2 - Dados pessoais
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/Markov.ps.Z, 19980121 Semi-pullbacks in Categories of Markov Processes Abbas Edalat Department of Computing Imperial College of Science, Technology and Medicine 180 Queen's Gate London SW7 2BZ UK ae@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Hodkinson/TM_course/ch11-12_allfonts.ps.gz, 19980123 142 11 Reduction in p-time We now use Turing machines to formalise the technique we saw in 8.6 of reducing one problem to another in p-time. This p-time reduction gives fast non-deterministic solutions to new yes/no problems from known fast nondeterministic solutions to old ones. We'll study its
	ftp://theory.doc.ic.ac.uk/theory/papers/Spurr/DRUMS/Volume2/Volume2.ps, 19980127 CONTENTS PHILIPPE BESNARD AND ANTHONY HUNTER Introduction to Actual and Potential Contradictions 1 ANTHONY HUNTER Paraconsistent Logics 11 J.-J. CH. MEYER AND W. VAN DER HOEK Modal Logics for Representing Incoherent Knowledge 37 TORSTEN SCHAUB The Family of Default Logics 77 JAMES P. DELGRANDE
	ftp://theory.doc.ic.ac.uk/theory/papers/Duarte/misc/curric2.ps.gz, 19980129 Curriculum Vitae (R esum e) Carlos Henrique Cabral Duarte January 29, 1998 Curriculum Vitae - Carlos H. C. Duarte 1 1 - Identification 1. Name: Carlos Henrique Cabral Duarte 2. Date of birth: 01/July/1970 3. City of birth: Juiz de Fora, MG, Brazil 4. Nationality: Brazilian citizen 5. Passport: C F
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/dimensionshort.ps.Z, 19980206 An Algorithm to Estimate the Hausdorff Dimension of Self-Affine Sets Abbas Edalat Department of Computing, Imperial College, 180 Queen's gate, London SW7 2BZ. ae@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/paper.ps.gz, 19980210 Semantics of Exact Real Arithmetic Peter John Potts Abbas Edalat Mart n H otzel Escard o Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK fpjp,ae,mheg@doc.ic.ac.uk
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/extensionofvaluations.ps.Z, 19980225 An extension result for continuous valuations M. Alvarez-Manilla , A. Edalat , N. Saheb-Djahromi y Wednesday 25 th February 1998
	ftp://theory.doc.ic.ac.uk/theory/papers/Lano/rvb.ps, 19980227 Reverse-Engineering COBOL via Formal Methods K. Lano P.T. Breuer H. Haughtony August 1991
	ftp://theory.doc.ic.ac.uk/theory/papers/Edalat/bisim.ps.gz, 19980302 Bisimulation for Labeled Markov Processes Richard Blute Department of Mathematics University of Ottawa Ottawa, Ontario, Canada rblute@mathstat.uottawa.ca Abbas Edalaty Department of Computing Imperial College London, UK ae@doc.ic.ac.uk Jos ee Desharnais School of Computer Science McGill University