Browse

ftp://ftp.dcs.ed.ac.uk (237)

	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-199/ECS-LFCS-92-199.ps, 19921005 A Proof Assistant for Symbolic Model-Checking J. C. Bradfield Laboratory for Foundations of Computer Science University of Edinburgh The King's Buildings EDINBURGH U.K. EH9 3JZ email: jcb@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-275/ECS-LFCS-93-275.ps, 19931210 Multiple Inheritance via Intersection Types Adriana B. Compagnoni Catholic University, Nijmegen Benjamin C. Pierce LFCS, Edinburgh August 30, 1993 University of Edinburgh Technical Report ECS-LFCS-93-275 and Catholic University Nijmegen C.S. Department Technical Report 93-18
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-256/ECS-LFCS-93-256.ps, 19931210 Statically Typed Friendly Functions via Partially Abstract Types Benjamin C. Pierce INRIA-Roquencourt Benjamin.Pierce@inria.fr David N. Turner University of Edinburgh David.Turner@dcs.ed.ac.uk University of Edinburgh Technical Report ECS-LFCS-93-256 and INRIA-Roquencourt Rapport de Recherche No. 1899
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-273/ECS-LFCS-93-273.ps, 19931211 Structure and Behaviour in Hardware Verification1 K. G. W. Goossens Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, U.K.
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-261/ECS-LFCS-93-261.ps, 19931211 Decidability Questions for Bisimilarity of Petri Nets and Some Related Problems Petr Jan<=car Dept. of Computer Science, University of Ostrava Dvo<=r akova 7, 701 00 Ostrava 1, Czech Republic April 8, 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-260/ECS-LFCS-93-260.ps, 19931213 Simulated Annealing for Graph Bisection Mark Jerrum Gregory Sorkin y April 16, 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-272/ECS-LFCS-93-272.ps, 19931213 Uniform sampling modulo a group of symmetries using Markov chain simulation Mark Jerrum
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-259/ECS-LFCS-93-259.ps, 19931213 Approximately Counting Hamilton Cycles in Dense Graphs Martin Dyer Alan Friezey Carnegie Mellon University Mark Jerrumz University of Edinburgh 15th April 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-274/ECS-LFCS-93-274.ps, 19931213 On the decidability of model checking for several -calculi and Petri nets Javier Esparza Laboratory for Foundations of Computer Science University of Edinburgh King's Buildings Edinburgh EH9 3JZ e-mail: je@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-264/ECS-LFCS-93-264.ps, 19931214 Action Structures for the ss-Calculus Robin Milner Laboratory for Foundations of Computer Science, Computer Science Department, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, UK May 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-257/ECS-LFCS-93-257.ps, 19931214 Mistakes and Ambiguities in the Definition of Standard ML Stefan Kahrs University of Edinburgh Laboratory for Foundations of Computer Science King's Buildings, EH9 3JZ email: smk@dcs.ed.ac.uk Version of April 6, 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-269/ECS-LFCS-93-269.ps, 19931215 The Formalisation of a Hardware Description Language in a Proof System: Motivation and Applications1 K. G. W. Goossens Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, U.K. Email: kgg@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-270/ECS-LFCS-93-270.ps, 19940104 A Theory of Bisimulation for the ss-calculus Davide Sangiorgi Laboratory for Foundations of Computer Science Department of Computer Science, University of Edinburgh The King's Buildings, Edinburgh EH9 3JZ, U.K. May 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-262/ECS-LFCS-93-262.ps, 19940105 Algebraic Theories for Name-Passing Calculi Joachim Parrow Davide Sangiorgiy April 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-219/ECS-LFCS-92-219.ps, 19940106 Unlimp Uniqueness as a Leitmotiv for Implementation Stefan Kahrs University of Edinburgh Laboratory for Foundations of Computer Science King's Buildings, EH9 3JZ email: smk@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-249/ECS-LFCS-92-249.ps, 19940106 Action Structures Robin Milner Laboratory for Foundations of Computer Science, Computer Science Department, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, UK December 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-238/ECS-LFCS-92-238.ps, 19940106 Polymorphic Type Checking by Interpretation of Code Stefan Kahrs University of Edinburgh Laboratory for Foundations of Computer Science King's Buildings, EH9 3JZ email: smk@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-251/ECS-LFCS-92-251.ps, 19940107 Equivalences between Logics and their Representing Type Theories Philippa Gardnery
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-243/ECS-LFCS-92-243.ps, 19940109 The Virtues of Eta-expansion C. Barry Jay 1 Computing Methods Unit School of Computing Sciences University of Technology Sydney PO Box 123 Broadway 2007 Australia. e-mail: cbj@socs.uts.edu.au Neil Ghani LFCS, Department of Computer Science University of Edinburgh The King's Buildings, Mayfield Road
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-162/ECS-LFCS-91-162.ps, 19940112 A Framework for Defining Logics Robert Harper Furio Honselly Gordon Plotkinz
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-236/ECS-LFCS-92-236.ps, 19940112 Parsing in the SML Kit Nick Rothwell September 10, 1992 1 Introduction This document describes the parsing scheme of the SML Kit. We introduce the grammar datatype, or abstract syntax, and the grammar specification itself, explaining the conventions used. There are various mechanisms employed to resolve
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-237/ECS-LFCS-92-237.ps, 19940112 Miscellaneous Design Issues in the ML Kit Nick Rothwell September 10, 1992 1 Introduction This document covers a number of assorted design topics involving the ML Kit. These issues are sufficiently small that they do not merit reports of their own, and yet it is important that they be covered in order
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-252/ECS-LFCS-92-252.ps, 19940112 Newtonian Arbiters Cannot be Proven Correct Michael Mendler y Institute for Computer-Aided Circuit Design University of Erlangen, FRG. Terry Stroup z Laboratory for Foundations of Computer Science University of Edinburgh, UK
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-235/ECS-LFCS-92-235.ps, 19940112 Functional Compilation from the Standard ML Core Language to Lambda Calculus Nick Rothwell September 10, 1992 1 Introduction This paper describes a compiler from the SML core language to a simple intermediate code based on the lambda calculus. It forms an optional part of the SML Kit, and the interface
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-240/ECS-LFCS-92-240.ps, 19940125 Observational Equivalence and Compiler Correctness Fabio Q. B. da Silva Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh, Scotland, U.K., e-mail: fabio@dcs.ed.ac.uk September 18, 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-285/ECS-LFCS-94-285.ps, 19940211 The Mobility Workbench A Tool for the ss-Calculus Bj orn Victory Uppsala University and Swedish Institute for Computer Science Faron Mollerz University of Edinburgh February 2, 1994x
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-281/ECS-LFCS-94-281.ps, 19940211 Subtyping in F ^ is decidable Adriana B. Compagnoni LFCS University of Edinburgh Technical Report ECS-LFCS-94-281 January 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-280/ECS-LFCS-94-280.ps, 19940211 Higher-Order Subtyping Martin Steffen Benjamin Piercey February 2, 1994 University of Edinburgh Technical Report ECS-LFCS-94-280 and IMMD VII, Universit at Erlangen-N urnberg Interner Bericht IMMD7-01/94 Revised version with Fun subtyping
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-281/Castagna.ps, 19940211 Decidable Bounded Quantification Giuseppe Castagna LIENS(CNRS)-DMI castagna@dmi.ens.fr Benjamin C. Piercey LFCS, Univ. of Edinburgh bcp@dcs.ed.ac.uk January 10, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-284/ECS-LFCS-94-284.ps, 19940214 First-Class Polymorphism for ML Stefan Kahrs University of Edinburgh Laboratory for Foundations of Computer Science King's Buildings, EH9 3JZ email: smk@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-282/ECS-LFCS-94-282.ps, 19940215 Locality and Non-interleaving Semantics in calculi for mobile processes Davide Sangiorgi y January 29, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/86/ECS-LFCS-86-17/ECS-LFCS-86-17.ps, 19940302 Toward formal development of programs from algebraic specifications: implementations revisited1 Donald Sannella2 and Andrzej Tarlecki3
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-71/ECS-LFCS-89-71.ps, 19940302 Toward formal development of ML programs: foundations and methodology \| Preliminary versiony \| Donald Sannella Andrzej Tarlecki Laboratory for Foundations of Computer Science Institute of Computer Science Department of Computer Science Polish Academy of Sciences University of Edinburgh Warsaw
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-75/ECS-LFCS-89-75.ps, 19940302 Structured theory presentations and logic representations Robert Harpery Donald Sannellaz Andrzej Tarleckix Draft: 10th December 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-283/ECS-LFCS-94-283.ps, 19940302 Interfaces and Extended ML Stefan Kahrs Donald Sannellay Andrzej Tarleckiz
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/86/ECS-LFCS-86-15/ECS-LFCS-86-15.ps, 19940302 Formal specification of ML programs Donald Sannella Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh 1 Introduction Specifications play a part in every phase of program development. First, the construction of a program cannot commence without a
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-102/ECS-LFCS-89-102.ps, 19940302 1 Formal program development in Extended ML for the working programmer Donald Sannellay
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-204/ECS-LFCS-92-204.ps, 19940302 Toward Formal Development of Programs from Algebraic Specifications: Model{Theoretic Foundations1 Donald Sannella Department of Computer Science University of Edinburgh Edinburgh, UK Andrzej Tarlecki Institute of Computer Science Polish Academy of Sciences Warsaw, Poland
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-138/ECS-LFCS-91-138.ps, 19940302 Extended ML: Past, present and future Donald Sannella Andrzej Tarleckiy
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/86/ECS-LFCS-86-16/ECS-LFCS-86-16.ps, 19940302 Extended ML: an institution-independent framework for formal program development Donald Sannella1 and Andrzej Tarlecki2
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-286/ECS-LFCS-94-286.ps, 19940331 A polynomial algorithm for deciding bisimilarity of normed context-free processes Yoram Hirshfeld Mark Jerrumy Faron Mollerz Department of Computer Science, University of Edinburgh, The King's Buildings, Mayfield Road, Edinburgh EH9 3JZ, Scotland Dedicated to Robin Milner on the occasion of his 60th
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-288/ECS-LFCS-94-288.ps, 19940422 A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes Yoram Hirshfeld School of Mathematics and Computer Science Tel Aviv University Israel Mark Jerrumy Department of Computer Science University of Edinburgh United Kingdom Faron Mollerz Swedish Institute of
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-290/ECS-LFCS-94-290.ps, 19940422 A very simple algorithm for estimating the number of k-colourings of a low-degree graph. Mark Jerrum Department of Computer Science University of Edinburgh United Kingdom April 22, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-289/ECS-LFCS-94-289.ps, 19940424 Why tricategories A.J.Power Department of Computer Science University of Edinburgh King's Buildings Edinburgh EH9 3JZ Scotland. April 11, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-186/ECS-LFCS-91-186.ps, 19940608 Modelling British Rail's Interlocking Logic: Geographic Data Correctness M. J. Morley Laboratory for Foundations of Computer Science Department of Computer Science, University of Edinburgh Edinburgh EH9 3JZ. e-mail: mjm@lfcs.ed.ac.uk November 1991 (Revision: July 10, 1993)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-291/ECS-LFCS-94-291.ps, 19940614 Congruences in Commutative Semigroups Joram Hirshfeld December 6, 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-292/ECS-LFCS-94-292.ps, 19940614 Improved approximation algorithms for MAX k-CUT and MAX BISECTION Alan Frieze Carnegie Mellon University Mark Jerrumy University of Edinburgh 6th June, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/90/ECS-LFCS-90-109/ECS-LFCS-90-109.ps, 19940614 Tactics for State Space Reduction on the Concurrency Workbench Matthew J. Morley February 1990
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/o.ps, 19940727 LFCS LFCS LFCS O
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/w.ps, 19940727 LFCS LFCS LFCS W
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/k.ps, 19940727 LFCS LFCS LFCS K
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1989.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1989
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/n.ps, 19940727 LFCS LFCS LFCS N
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1991.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/j.ps, 19940727 LFCS LFCS LFCS J
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1994.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/t.ps, 19940727 LFCS LFCS LFCS T
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/h.ps, 19940727 LFCS LFCS LFCS H
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/r.ps, 19940727 LFCS LFCS LFCS R
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/f.ps, 19940727 LFCS LFCS LFCS F
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/l.ps, 19940727 LFCS LFCS LFCS L
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/i.ps, 19940727 LFCS LFCS LFCS I
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/y.ps, 19940727 LFCS LFCS LFCS Y
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/m.ps, 19940727 LFCS LFCS LFCS M
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/g.ps, 19940727 LFCS LFCS LFCS G
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1987.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1987
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/s.ps, 19940727 LFCS LFCS LFCS S
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/u.ps, 19940727 LFCS LFCS LFCS U
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1992.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/q.ps, 19940727 LFCS LFCS LFCS O
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/e.ps, 19940727 LFCS LFCS LFCS E
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1986.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1986
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1990.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1990
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/v.ps, 19940727 LFCS LFCS LFCS V
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1995.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/p.ps, 19940727 LFCS LFCS LFCS P
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1993.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/1988.ps, 19940727 LFCS LFCSLFCS LFCSLFCSLFLFLFLFCS 1988
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/x.ps, 19940727 LFCS LFCS LFCS X
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/z.ps, 19940727 LFCS LFCS LFCS Z
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/icons/oldicons/figs/reports-title.ps, 19940727 F C SL aboratory for oundations of omputer cience REPORTS
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-294/ECS-LFCS-94-294.ps, 19940902 Deciding equivalences in simple Process Algebras. Yoram Hirshfeld Tel Aviv University July 23, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-296/ECS-LFCS-94-296.ps, 19940902 The computational complexity of counting Mark Jerrumy Department of Computer Science University of Edinburgh 28th July 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-293/ECS-LFCS-94-293.ps, 19940903 On modal mu-calculus and B uchi tree automata Roope Kaivola University of Edinburgh Laboratory for Foundations of Computer Science
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-304/ECS-LFCS-94-304.ps, 19940912 A Typed Operational Semantics for Type Theory Healfdene Goguen Doctor of Philosophy University of Edinburgh 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-301/ECS-LFCS-94-301.ps, 19940912 An Old Sub-Quadratic Algorithm for Finding Extremal Sets Paul Pritchard
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-305/ECS-LFCS-94-305.ps, 19940913 Balancing load under large and fast load changes in distributed computing systems - A case study Thierry Le Sergenty and Bernard Berthomieuz
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-306/ECS-LFCS-94-306.ps, 19940913 Adaptive selection of protocols for strict coherency in distributed shared memory Thierry Le Sergent and David C.J. Matthewsy LFCS, University of Edinburgh.
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-298/ECS-LFCS-94-298.ps, 19940914 High undecidability of weak bisimilarity for Petri nets Petr Jan<=car Dept. of Computer Science, University of Ostrava Dvo<=r akova 7, 701 00 Ostrava 1, Czech Republic e-mail: jancar@oudec.osu.cz August 8, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-209/ECS-LFCS-92-209.ps, 19940928 Inductive Data Types: Well-ordering Types Revisited Healfdene Goguen Zhaohui Luo LFCS, Dept. of Computer Science, Edinburgh Univ.
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-73/ECS-LFCS-89-73.ps, 19941009 Mads Tofte, March 1, 1989 Laboratory for Foundations of Computer Science Department of Computer Science Edinburgh University Four Lectures on Standard ML The following notes give an overview of Standard ML with emphasis placed on the Modules part of the language. The notes are, to the best of my
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-300/ECS-LFCS-94-300.ps, 19941101 The Definition of Extended ML Stefan Kahrs Donald Sannella Andrzej Tarleckiy \| Version 1 \|
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/86/ECS-LFCS-86-14/ECS-LFCS-86-14.ps, 19941107 Introduction to Standard ML Robert Harper (With exercises by Kevin Mitchell1) School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 1Laboratory for Foundations of Computer Science, Edinburgh University, Edinburgh EH9 3JZ, United Kingdom Contents 1 Introduction 1 2 The Core Language
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-313/ECS-LFCS-94-313.ps, 19941216 Generating and counting Hamilton cycles in random regular graphs Alan Frieze Mark Jerrumy Michael Molloyz Robert Robinsonx Nicholas Wormald{ December 14, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-317/ECS-LFCS-95-317.ps, 19950126 Computational P olya theory Mark Jerrumy Department of Computer Science University of Edinburgh United Kingdom
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-278/ECS-LFCS-93-278.ps, 19950126 Decidability and Decomposition in Process Algebras Soren Christensen Doctor of Philosophy University of Edinburgh 1993 (Graduation Date: September 1993)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-316/ECS-LFCS-95-316.ps, 19950127 1 LEMMA Interface Definition David C.J. Matthews and Thierry Le Sergent
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-314/ECS-LFCS-95-314.ps, 19950127 Towards a Domain Theory for Termination Proofs Stefan Kahrs University of Edinburgh Laboratory for Foundations of Computer Science King's Buildings, EH9 3JZ email: smk@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-318/ECS-LFCS-95-318.ps, 19950127 1 On behavioural abstraction and behavioural satisfaction in higher-order logic Martin Hofmanny and Donald Sannellaz Laboratory for Foundations of Computer Science University of Edinburgh
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-315/ECS-LFCS-95-315.ps, 19950131 Correct Separate and Selective Closure Conversion Paul Steckler Keywords: dataflow analysis, escape analysis, closure conversion, modules, regular trees
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-312/ECS-LFCS-94-312.ps, 19950222 Multiple Values in Standard ML Kevin Mitchell LFCS, Department of Computer Science University of Edinburgh
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-311/ECS-LFCS-94-311.ps, 19950222 Concurrency in a Natural Semantics Kevin Mitchell LFCS, Department of Computer Science University of Edinburgh
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-320/ECS-LFCS-95-320.ps, 19950225 Typing Abstract Data Types Judith Underwood February 20, 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-309/ECS-LFCS-94-309.ps, 19950225 On Computing the Subset Graph of a Collection of Sets Paul Pritchard
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-319/ECS-LFCS-95-319.ps, 19950225 Proof and Design Machine-assisted Formal Proof as a Basis for Behavioural Design Tools Michael P. Fourman Laboratory for Foundations of Computer Science, The University of Edinburgh, King's Buildings, Edinburgh EH9 3JZ Michael.Fourman@ed.ac.uk Summary. We describe a formalisation of the design process,
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-321/ECS-LFCS-95-321.ps, 19950225 Tableau for Intuitionistic Predicate Logic as Metatheory Judith Underwood February 20, 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-301/ECS-LFCS-94-301-revised.ps, 19950225 An Old Sub-Quadratic Algorithm for Finding Extremal Sets Paul Pritchard 1 Department of Computer Science, University of Edinburgh, King's Buildings, Edinburgh EH9 3JZ, United Kingdom
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-310/ECS-LFCS-94-310.ps, 19950225 Supporting Formal Reasoning about Standard ML Graham Collins Stephen Gilmore November 11, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-302/ECS-LFCS-94-302.ps, 19950226 Decidability of model checking for infinite-state concurrent systems Javier Esparza Laboratory for Foundations of Computer Science University of Edinburgh August 26, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-180/ECS-LFCS-91-180.ps, 19950228 The Polyadic ss-Calculus: a Tutorial Robin Milner Laboratory for Foundations of Computer Science, Computer Science Department, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, UK October 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-139/ECS-LFCS-91-139.ps, 19950301 A kernel specification formalism with higher-order parameterisation Donald Sannellay Andrzej Tarleckiz
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/86/ECS-LFCS-86-21/ECS-LFCS-86-21.ps, 19950301 Some thoughts on algebraic specification1;2 Donald Sannella and Andrzej Tarlecki3 Department of Computer Science University of Edinburgh 1 Introduction This paper presents in an informal way the main ideas underlying our work on algebraic specification. The central idea, due to Goguen and Burstall, is
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-303/ECS-LFCS-94-303.ps, 19950302 Positive Subtyping Martin Hofmann Benjamin Piercey September 7, 1994 ECS-LFCS-94-303
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-307/ECS-LFCS-94-307.ps, 19950302 Axiomatic Domain Theory in Categories of Partial Maps Marcelo P. Fiore Doctor of Philosophy University of Edinburgh June 1994 (Graduation date November 1994) Dedicado a mis padres, Cristina y Luis, y a mis hermanos, Ver onica y Alejandro. c Marcelo P. Fiore Synopsis This thesis is an investigation into
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-308/ECS-LFCS-94-308.ps, 19950302 The Proof Theory and Semantics of Intuitionistic Modal Logic Alex K. Simpson Doctor of Philosophy University of Edinburgh 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-297/ECS-LFCS-94-297.ps, 19950302 A fully abstract semantics for causality in the ss-calculus Michele Boreale Davide Sangiorgi Dipartimento di Scienze dell'Informazione Department of Computer Science Universit a di Roma La Sapienza" University of Edinburgh
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-299/ECS-LFCS-94-299.ps, 19950302 On the Bisimulation Proof Method Davide Sangiorgi Laboratory for Foundations of Computer Science Department of Computer Science, University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, U.K. Email: sad@dcs.ed.ac.uk. November 20, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-211/ECS-LFCS-92-211.ps, 19950307 LEGO Proof Development System: User's Manual Zhaohui Luo Robert Pollack Department of Computer Science University of Edinburgh May 7, 1992 1 Contents 1 Introduction 5 2 The Working Environment 8 2.1 Loading and exiting LEGO : : : : : : : : : : : : : : : : : : : : : : 8 2.2 Lego state and proof state : :
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-247/ECS-LFCS-92-247_3.ps, 19950307 Chapter 4 Examples To illustrate the discussion of the previous chapter, we now turn to some examples of the use of deliverables in small-scale program development. The use of deliverables may seem heavy-handed and even counter-productive for the smaller examples we have considered, but we hope that the
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-247/ECS-LFCS-92-247_1.ps, 19950307 Deliverables: a categorical approach to program development in type theory James Hugh McKinna Doctor of Philosophy University of Edinburgh 1992 le hasard ne favorise que les esprits pr epar es Pasteur
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-247/ECS-LFCS-92-247_2.ps, 19950307 Chapter 3 First-order and second-order deliverables In this chapter, we consider the basic syntactic definitions in the study of this approach to program correctness. As indicated in the introduction, we wish to give an account of correct programs (with respect to some specification) in a way whichmakes
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-247/ECS-LFCS-92-247_4.ps, 19950307 Chapter 6 Further work and conclusions 6.1 Partial equivalence relations and observational equivalence The basic definitions of Chapter 3 contain a lot of redundancy, as far as proofs are concerned. Having chosen a notion of equality sufficient to give a smooth theory of the categorical structure of
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-131/ECS-LFCS-91-131.ps, 19950307 Program Specification and Data Refinement in Type Theory Zhaohui Luo Department of Computer Science, University of Edinburgh JCMB, KB, Mayfield Rd., Edinburgh EH9 3JZ, U.K. January 21, 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-247/ECS-LFCS-92-247_5.ps, 19950307 Appendix B. LEGO code relevant to this thesis 197 B.3 Examples B.3.1 A simple example We recall the introductory example of Chapter 2, of a simple doubling function. ; venZ:Phi Z}
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-225/PierceTurner94.ps, 19950308 J. Functional Programming 1 (1): 1{000, January 1993 c 1993 Cambridge University Press 1 Simple Type-Theoretic Foundations For Object-Oriented Programming Benjamin C. Pierce David N. Turner Department of Computer Science, University of Edinburgh, The King's Buildings, Edinburgh, EH9 3JZ, U.K.
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/88/ECS-LFCS-88-56/ECS-LFCS-88-56.ps, 19950308 A survey of formal software development methods1 Donald Sannella Department of Artificial Intelligence and Department of Computer Science University of Edinburgh July 1988 1 Introduction 1.1 Scope This paper is a survey of the current state of the art of research on methods for formal software
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-225/PierceTurner93a.ps, 19950308 Object-Oriented Programming Without Recursive Types Benjamin C. Pierce David N. Turnery LFCS, University of Edinburgh
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-234/ECS-LFCS-92-234.ps, 19950308 A Fast Communication Algorithm for the Completely Connected Optical Communication Parallel Computer Leslie Ann Goldbergy and Mark Jerrumz August 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-215/ECS-LFCS-92-215.ps, 19950308 Building domains from graph models Wesley Phoa Laboratory for the Foundations of Computer Science James Clerk Maxwell Building, The King's Buildings Edinburgh EH9 3JZ, Scotland
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/88/ECS-LFCS-88-55/ECS-LFCS-88-55.ps, 19950308 Unifying Exceptions with Constructors in Standard ML Andrew Appel, David MacQueen, Robin Milner, Mads Tofte May 30, 1988 1 Introduction The Standard ML Core Language, as described in , was modified by several changes detailed in . It was declared in that, with one exception, all later changes
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-213/ECS-LFCS-92-213.ps, 19950308 A proposed categorical semantics for Pure ML Wesley Phoa and Michael Fourman Laboratory for the Foundations of Computer Science James Clerk Maxwell Building, The King's Buildings Edinburgh EH9 3JZ, Scotland
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-228/ECS-LFCS-92-228.ps, 19950308 Formal Development of Functional Programs in Type Theory \| A Case Study Martin Hofmann Department of Computer Science, University of Edinburgh JCMB, KB, Mayfield Rd., Edinburgh EH9 3JZ, Scotland July 31, 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-222/ECS-LFCS-92-222.ps, 19950308 Toward formal development of programs from algebraic specifications: parameterisation revisited Donald Sannellay Stefan Soko lowskiz Andrzej Tarleckix
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-226/ECS-LFCS-92-226.ps, 19950308 An Abstract View of Objects and Subtyping (Preliminary Report) Martin Hofmann Benjamin Pierce Department of Computer Science University of Edinburgh The King's Buildings Edinburgh, EH9 3JZ, U.K. August 31, 1992 ECS-LFCS-92-226
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-135/ECS-LFCS-91-135.ps, 19950309 To appear in: Proc. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Brighton, April 1991 (Springer Lecture Notes in Computer Science). Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL1 Bernd Krieg-Br
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-223/ECS-LFCS-92-223_revised.ps, 19950309 Relational Parametricity and Local Variables (Preliminary Report) P. W. O'Hearn Computer and Information Science Syracuse University Syracuse, New York, U.S.A. 13244 ohearn@top.cis.syr.edu R. D. Tennenty Laboratory for Foundations of Computer Science Department of Computer Science University of
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-192/ECS-LFCS-92-192_revised.ps, 19950309 Semantics of Local Variables P. W. O'Hearn R. D. Tennent y
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-204/ECS-LFCS-92-204_revised.ps, 19950309 Model-theoretic foundations for program development: basic concepts and motivation Donald Sannella Department of Computer Science University of Edinburgh Edinburgh, UK. e-mail : dts@dcs.ed.ac.uk Andrzej Tarlecki Institute of Informatics Warsaw University and Institute of Computer Science Polish Academy
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-193/ECS-LFCS-92-193.ps, 19950309 Verification of Parallel Systems via Decomposition Jan Friso Grootey Faron Mollerz CWI, Amsterdam University of Edinburgh
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-221/ECS-LFCS-92-221.ps, 19950310 Modal and Temporal Logics for Processes Colin Stirling Dept. of Computer Science University of Edinburgh Edinburgh EH9 3JZ, UK email: cps@uk.ac.ed.dcs Preface In the following we examine modal and temporal logics for processes. First in section 1 we introduce concurrent processes as terms of an
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-223/ECS-LFCS-92-223_revised_2.ps, 19950310 Parametricity and Local Variables P. W. O'Hearn School of Computer and Information Science Syracuse University Syracuse, New York, U.S.A. 13244 ohearn@top.cis.syr.edu R. D. Tennenty Department of Computing and Information Science Queen's University Kingston, Ontario, Canada K7L 3N6 rdt@qucis.queensu.ca
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-175/ECS-LFCS-91-175.ps, 19950310 A Language and Translator for Value-passing CCS Glenn Bruns December 5, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/94/ECS-LFCS-94-287/ECS-LFCS-94-287.ps, 19950310 Applying Process Refinement to a Safety-Relevant System Glenn Bruns Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, UK April 14, 1994 1 Introduction Development by sound refinement steps is an important method for showing the correctness of a system relative to its
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/90/ECS-LFCS-90-119/ECS-LFCS-90-119.ps, 19950310 Relevance Logic and Concurrent Composition Mads Frederik Dam Ph. D. University of Edinburgh 1989 (Graduation date November 1990)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/90/ECS-LFCS-90-105/ECS-LFCS-90-105.ps, 19950310 Probabilistic Non-determinism Claire Jones Doctor of Philosophy University of Edinburgh August 1989 (Graduation Date July 1990)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-239/ECS-LFCS-92-239.ps, 19950310 A Case Study in Safety-Critical Design Glenn Bruns Department of Computer Science, University of Edinburgh Edinburgh EH9 3JZ, UK
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-242/ECS-LFCS-92-242.ps, 19950312 Deliverables: a categorical approach to program development in type theory Rod Burstall and James McKinna1 Laboratory for the Foundations of Computer Science University of Edinburgh2 August 15, 1992 1 Introduction This paper outlines a method for constructing a program together with a proof of its
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/88/ECS-LFCS-88-66/ECS-LFCS-88-66_revised.ps, 19950320 Computational lambda-calculus and monads Eugenio Moggi Lab. for Found. of Comp. Sci. University of Edinburgh EH9 3JZ Edinburgh, UK On leave from Univ. di Pisa
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/88/ECS-LFCS-88-63/ECS-LFCS-88-63.ps.gz, 19950320 The Partial Lambda-Calculus Eugenio Moggi Ph. D. University of Edinburgh 1988
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps, 19950320 An introduction to fibrations, topos theory, the effective topos and modest sets Wesley Phoa wkp@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-99/ECS-LFCS-89-99.ps, 19950320 Compositional Characterization of Observable Program Properties Bernhard Steffen C. Barry Jay y Michael Mendlerz
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/90/ECS-LFCS-90-112/ECS-LFCS-90-112_revised.ps, 19950320 Higher-Order Modules and the Phase Distinction Robert Harper Carnegie Mellon University Pittsburgh, PA 15213 John C. Mitchell Stanford University Stanford, CA 94305 Eugenio Moggi University of Edinburgh Edinburgh EH9-3JZ, U.K.
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-232/ECS-LFCS-92-232_revised.ps, 19950320 To appear in: Theoretical Computer Science (1994), Proceedings MFPS8. On the ss-Calculus and Linear Logic G. Bellin P. J. Scott y July 20, 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-158/ECS-LFCS-91-158_revised.ps.gz, 19950320 Logic Programming in a Fragment of Intuitionistic Linear Logic Joshua S. Hodas Computer Science Department Harvey Mudd College Claremont, CA 91711-5990 USA hodas@cs.hmc.edu Dale Miller Computer Science Department University of Pennsylvania Philadelphia, PA 19104-6389 USA dale@saul.cis.upenn.edu
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-160/ECS-LFCS-91-160.ps, 19950320 Unification of Simply Typed Lambda-Terms as Logic Programming Dale Miller Laboratory for the Foundation of Computer Science University of Edinburgh, and Computer Science Department University of Pennsylvania March 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-163/thesis.ps, 19950320 Generating Program Animators from Programming Language Semantics Dave Berry Ph. D. University of Edinburgh 1991 (Graduation date July 1991)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-155/ECS-LFCS-91-155.ps, 19950320 Embedding a CHDDL in a Proof System K. G. W. Goossens Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh The King's Buildings Edinburgh EH9 3JZ, Scotland, U.K. March 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-214/ECS-LFCS-92-214.ps, 19950320 From term models to domains Wesley Phoa Laboratory for the Foundations of Computer Science James Clerk Maxwell Building, The King's Buildings Edinburgh EH9 3JZ, Scotland
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-213/ECS-LFCS-92-213_revised.ps, 19950320 A proposed categorical semantics for Pure ML Wesley Phoa and Michael Fourman Laboratory for the Foundations of Computer Science James Clerk Maxwell Building, The King's Buildings Edinburgh EH9 3JZ, Scotland
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/90/ECS-LFCS-90-113/ECS-LFCS-90-113.ps, 19950320 An Abstract View of Programming Languages 1 Eugenio Moggi Lab. for Found. of Comp. Sci. University of Edinburgh EH9 3JZ Edinburgh, UK em@lfcs.edinburgh.ac.uk June 1989 1These Notes were produced at Stanford University as part of the course CS 359 taught in Spring Term 1989. A special thank to John
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-197/ECS-LFCS-92-197_revised.ps, 19950322 Parallel Processing Letters c World Scientific Publishing Company UNIMODULARITY AND THE PARALLELIZATION OF LOOPS MICHAEL BARNETT Laboratory for Applied Logic Department of Computer Science University of Idaho Moscow, Idaho 83843, U.S.A. and CHRISTIAN LENGAUER Fakult at f ur Mathematik und Informatik
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-200/ECS-LFCS-92-200_revised.ps, 19950322 Intersection Types and Bounded Polymorphism Benjamin C. Pierce Department of Computer Science King's Buildings Edinburgh, EH9 3JZ United Kingdom bcp@dcs.ed.ac.uk August 24, 1993
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-201/ECS-LFCS-92-201.ps, 19950322 Approximating the Permanent: a Simple Approach Lars Eilstrup Rasmussen March 12, 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-178/ECS-LFCS-91-178.ps, 19950329 Improved bounds for mixing rates of Markov chains on combinatorial structures Alistair Sinclair Department of Computer Science, University of Edinburgh The King's Buildings, Edinburgh EH9 3JZ, Scotland July 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-177/ECS-LFCS-91-177.ps, 19950417 Modularising the Specification of a Small Database System in Extended ML Edmund Kazmierczak Department of Computer Science University of Edinburgh Edinburgh, EH9 3JZ email : eka@lfcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-147/ECS-LFCS-91-147.ps, 19950418 CORRECTNESS-ORIENTED APPROACHES TO SOFTWARE DEVELOPMENT A thesis submitted in fulfilment of the requirements for the degree of Doctor of Philosophy in the Faculty of Science of The Queen's University of Belfast By Stephen Gilmore, BSc. September 1990 (Graduation date July 1991) First printing: April
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-268/ECS-LFCS-93-268.ps, 19950505 Embedding Hardware Description Languages in Proof Systems Kees G. W. Goossens Doctor of Philosophy University of Edinburgh 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/92/ECS-LFCS-92-231/ECS-LFCS-92-231.ps, 19950505 Operational Semantics Based Formal Symbolic Simulation K. G. W. Goossens Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh The King's Buildings Edinburgh EH9 3JZ, Scotland, U.K. August 1992
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/90/ECS-LFCS-90-115/ECS-LFCS-90-115.ps, 19950525 Theoretical Computer Science 96 (1992) 157{174 LOCAL MODEL CHECKING FOR INFINITE STATE SPACES Julian BRADFIELD and Colin STIRLING Department of Computer Science, University of Edinburgh, The King's Buildings, EDINBURGH, U.K. EH9 3JZ Abstract. We present a sound and complete tableau proof system for
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-333/CHARME95/iwls95a.ps.Z, 19950718 Formal Design of a Class of Computers \| its high stage: abstract microprogramming Li-Guo Wang1 Department of Computer Science, University of Edinburgh, Michael Mendler2 Department of Computer Science, Technical University of Denmark,
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-322/ECS-LFCS-95-322.ps, 19951013 The definition of Extended ML: a gentle introduction Stefan Kahrsy Donald Sannellaz Andrzej Tarleckix
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-337/ECS-LFCS-95-337.ps, 19951103 An effective tableau system for the linear time mu-calculus Julian Bradfieldy, Javier Esparzaz, Angelika Maderz
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-325/ECS-LFCS-95-325.ps, 19951122 LEMMA: A Distributed Shared Memory with Global and Local Garbage Collection David C. J. Matthews, Thierry Le Sergent, University of Edinburgh, LAAS-CNRS
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-174/ECS-LFCS-91-174.ps, 19951122 1 A Distributed Concurrent Implementation of Standard ML LFCS Report ECS-LFCS-91-174 David C.J. Matthews Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh dcjm@lfcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-326/ECS-LFCS-95-326.ps, 19951207 A quasi-polynomial-time algorithm for sampling words from a context-free language Vivek Gore and Mark Jerrum Department of Computer Science University of Edinburgh 1st July, 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-323/ECS-LFCS-95-323.ps, 19951208 The Theory of LEGO A Proof Checker for the Extended Calculus of Constructions Robert Pollack Doctor of Philosophy University of Edinburgh 1994 Atomics is a very intricate theorem and can be worked out with algebra but you wouldwant to take it by degrees because you might spend the whole night proving a
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-327/ECS-LFCS-95-327.ps, 19951208 Extensional concepts in intensional type theory Martin Hofmann Doctor of Philosophy University of Edinburgh 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-324/ECS-LFCS-95-324.ps, 19951208 Axiomatising Linear Time Mu-calculus Roope Kaivola Laboratory for Foundations of Computer Science University of Edinburgh The King's Buildings, Edinburgh EH9 3JZ, United Kingdom
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-338/ECS-LFCS-95-338.ps, 19951211 On the expressivity of the modal mu-calculus J. C. Bradfield Laboratory for Foundations of Computer Science University of Edinburgh, The King's Buildings EDINBURGH, United Kingdom, EH9 3JZ email: jcb@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/87/ECS-LFCS-87-26/ECS-LFCS-87-26.ps, 19960212 Submodule Construction as Equation Solving in CCS Joachim Parrow Swedish Institute of Computer Science Box 1263, S-16428 Kista, Sweden
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-85/ECS-LFCS-89-85.ps, 19960212 A Calculus of Mobile Processes, Part I Robin Milner, University of Edinburgh, Scotland Joachim Parrow, Swedish Institute of Computer Science, Kista, Sweden David Walker, University of Technology, Sydney, Australia June 1989 (Revised September 1990) 1 Running title: Calculus of Mobile Processes, Part I
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/89/ECS-LFCS-89-86/ECS-LFCS-89-86.ps, 19960212 A Calculus of Mobile Processes, Part II Robin Milner, University of Edinburgh, Scotland Joachim Parrow, Swedish Institute of Computer Science, Kista, Sweden David Walker, University of Technology, Sydney, Australia June 1989 (Revised October 1990) 1 Running title: Calculus of Mobile Processes, Part II
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-328/ECS-LFCS-95-328.ps, 19960318 The Algebra of Finite State Processes Peter Michael Sewell Doctor of Philosophy University of Edinburgh 1995 Graduation date: November 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-330/ECS-LFCS-95-330.ps, 19960318 Lax naturality through enrichment Dedicated to Robert Gordon on the occasion of his 60th birthday Yoshiki Kinoshitayand John Powerz 26 December, 1994 Revised 26 July, 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-329/ECS-LFCS-95-329.safe.ps, 19960318 Formal Derivation of A Class of Computers Li-Guo Wang Doctor of Philosophy University of Edinburgh November 1994 i
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-329/ECS-LFCS-95-329.ps, 19960318 Formal Derivation of A Class of Computers Li-Guo Wang Doctor of Philosophy University of Edinburgh November 1994 i
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-2a.ps, 19960319 Exceptions with Parameters in Poly David C.J. Matthews This document is a suggestion on how to put exceptions with parameters into Poly. The idea is essentially that suggested by Alan Mycroft for Standard ML. 1 Background This can be skipped by those familiar with the ML exception mechanism. If we want
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-1a.ps, 19960319 The Poly and Poly/ML Distribution David C.J. Matthews 20 May 1988 1 Getting Started The Poly and Poly/ML distribution tape contains the basic system for running Poly and Standard ML. There are three files on the tape ffl driver ffl poly dbase ffl READ ME To build the system you need to read off the
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-339/ECS-LFCS-95-339.ps, 19960319 1 Adjoint Rewriting Neil Ghani Ph.D. University of Edinburgh Graduation November 1995 2 3
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-333/ECS-LFCS-95-333.ps, 19960319 Formal Design of a Class of Computers \| its high stage: abstract microprogramming3 Li-Guo Wang1 Department of Computer Science, University of Edinburgh, JCMB, The King's Buildings, Room 1414, Edinburgh EH9 3JZ, Scotland, U.K. E-mail: lgw@dcs.ed.ac.uk Michael Mendler2 Department of Computer Science,
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-4a.ps, 19960319 An Implementation of Standard ML in Poly David C.J. Matthews 1 Introduction This document describes an implementation of Standard ML written in Poly . This is a complete implementation of the language including the modules system. The original aim of the implementation was largely as an
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-336/ECS-LFCS-95-336.ps, 19960319 Universal Structure and a Categorical Framework for Type Theory Makoto Takeyama Doctor of Philosophy The University of Edinburgh February 1995 (Graduation date: May 1995)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-332/ECS-LFCS-95-332.ps, 19960319 Realizability Toposes and Language Semantics John R. Longley Doctor of Philosophy University of Edinburgh 1994
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-4f.ps, 19960319 Interfacing C Routines to Poly/ML David C.J. Matthews July 5, 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-3b.ps, 19960319 Progress with Persistence in Poly and Poly/ML David C.J. Matthews
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-334/ECS-LFCS-95-334.ps, 19960319 Abstraction of Hardware Construction August 21, 1995 Li-Guo Wang1 Room 1414, Department of Computer Science, University of Edinburgh, JCMB, The King's Buildings, Edinburgh EH9 3JZ, Scotland, U.K. E-mail: lgw@dcs.ed.ac.uk Michael Mendler2 Department of Computer Science, Technical University of Denmark,
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-331/ECS-LFCS-95-331.ps, 19960319 Enrichment and Representation Theorems for Categories of Domains and Continuous Functions Marcelo P. Fiore Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King's Buildings Edinburgh EH8 3JZ, Scotland March 1996 Synopsis
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-2c.ps, 19960319 Static and Dynamic Type-Checking David C.J. Matthews
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-2b.ps, 19960319 Structure-Editing in Poly and ML David C.J. Matthews This note is a suggestion for the way to proceed with structure-editing in Poly and/or ML. It should be relevant to both the Programming Logics project and to other work in Poly and ML. N.B. throughout this note I have used structure to mean a data
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-341/ECS-LFCS-96-341.ps, 19960319 Partial Functions in a Total Setting Simon Finn (simon@ahl.co.uk) Michael Fourman (M.Fourman@ed.ac.uk)y John Longley (jrl@lfcs.ed.ac.uk)y January 19, 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-4d.ps, 19960319 Hardware Support for Poly and ML David C.J. Matthews So far Poly has been implemented on the Vax and the Sun (MC68020) using native code. There is also a version which generates a byte code that can be interpreted. Even this version, however, was intended as an aid to porting the system from the Vax to
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-1c.ps, 19960319 Windows for ML. Revised. David C.J. Matthews 16 December 1987 This revised version of the windows system incorporates various changes and suggestions. It is still open to change but I hope it will soon converge on a standard. Any suggestions are welcome. The main aim is that it should be reasonably
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-4c.ps, 19960319 Machine Independent Optimisation in Poly and Poly/ML David C.J. Matthews 1 Introduction The Poly and Poly/ML code-generators generate a machine-independent code which is processed by an optimiser before being passed to a machine-dependent code-generator. The purpose of this note is to describe the
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-1b.ps, 19960319 Processes for Poly and ML David C.J. Matthews October 12, 1987 This document describes the process mechanism as it is currently implemented in Poly and ML. Though implementing processes in functional languages is interesting in itself the main motivation was the need to be able to handle asynchronous
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-340/ECS-LFCS-96-340.ps, 19960319 Detecting Local Channels in Distributed Poly/ML Paul Steckler Keywords: static analysis, escape analysis, concurrency, communication, locality, ML
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-3a.ps, 19960319 A Persistent Storage System for Poly and ML David C.J. Matthews
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-4e.ps, 19960319 The Poly and ML System: Low Level Support David C.J. Matthews 9 December 1987 1 Introduction This document forms part of a set describing the Poly and Standard ML systems. It is concerned with the low-level part of the system and the interface to the outside world. In particular it describes the
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/95/ECS-LFCS-95-335/ECS-LFCS-95-335-4b.ps, 19960319 The Poly and ML System: Abstract Machine and Realisation David C.J. Matthews July 5, 1995 1 Introduction This document forms part of a set describing the Poly and Standard ML systems. It describes the abstract machine and its realisation on the Vax and the MC68020 and on a interpreted byte-code
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/93/ECS-LFCS-93-271/ECS-LFCS-93-271.ps, 19960517 Timed Processes: Models, Axioms and Decidability Liang Chen Doctor of Philosophy University of Edinburgh 1992 i
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-185/ECS-LFCS-91-185.ps, 19960517 Decidability and Completeness in Real Time Process Algebra Liang Chen Laboratory for Foundations of Computer Science Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, Scotland cl@lfcs.dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/91/ECS-LFCS-91-184/ECS-LFCS-91-184.ps, 19960517 An Interleaving Model for Real-Time Systems Liang Chen1 Laboratory for the Foundations of Computer Science Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, UK September 15, 1991
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-343/ECS-LFCS-96-343.ps, 19960520 A New Approach to Polynomial-Time Generation of Random Points in Convex Bodies Russ Bubley Martin Dyer School of Computer Studies University of Leeds, Leeds LS2 9JT, England Mark Jerrum Department of Computer Science University of Edinburgh, Edinburgh EH9 3JZ, Scotland March 28, 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-344/ECS-LFCS-96-344.ps, 19960625 LFCS Laboratory for Foundations of Computer Science Department of Computer Science \| The University of Edinburgh Standard ML Type Generativity as Existential Quantification by Claudio V. Russo LFCS Report Series ECS{LFCS{96{344 LFCS June 1996 Department of Computer Science University of Edinburgh The
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-348/ECS-LFCS-96-348.ps, 19961025 Safety Assurance in Interlocking Design Matthew John Morley Doctor of Philosophy University of Edinburgh 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-346/ECS-LFCS-96-346.ps, 19961025 Computational applications of calculi based on monads Pietro Cenciarelli Doctor of Philosophy University of Edinburgh September 1995 (Graduation date: July 1996) A Giovanna e Renato
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-348/thesis-twoside.ps, 19961025 Safety Assurance in Interlocking Design Matthew John Morley Doctor of Philosophy University of Edinburgh 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-345/ECS-LFCS-96-345.ps, 19961025 The Polymorphic Pi-calculus: Theory and Implementation David N. Turner Ph. D. University of Edinburgh 1995
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-348/leamington.ps, 19961025 S35 T2T3 T4T5T8 T9 T22 T14/T14/T28 S37 P211 P224 P213 P225 S41 T7 P221 P223 P222 P228 P231 S57
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-347/ECS-LFCS-96-347.ps, 19961025 Dual Intuitionistic Linear Logic Andrew Barber Department of Computer Science University of Edinburgh September 23, 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-348/thesis-oneside.ps, 19961025 Safety Assurance in Interlocking Design Matthew John Morley Doctor of Philosophy University of Edinburgh 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-349/ECS-LFCS-96-349.ps, 19961111 The Swendsen-Wang process does not always mix rapidly Vivek K. Gore and Mark R. Jerrum Department of Computer Science University of Edinburgh 21st October, 1996
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/86/ECS-LFCS-86-1/ECS-LFCS-86-1.ps, 19961210 Is Computing an Experimental Science Robin Milner Text of the Inaugural Lecture of the Laboratory for Foundations of Computer Science1 We are beginning an ambitious programme of research into the Foundations of Computer Science. This isn't to say that we are beginning to study the theory of computation;
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/cut.ps, 19961211 p cxxc'xgbc'fdcxxxx(1)(2) bfdp xxxgbc'fdp cxxcxxxxc'x(3)(4)(b)(f)(f)(b)(f)g(b)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/graph.ps, 19961211 gbc'fdp cxxcxxxxc'xgbfdp xxx(f)(b)(f) (b)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/edge.ps, 19961211 n123nnn'n' 1n'n' 2(1)(2)(3) n123nn'n' 1n'n' 2n123nn'n' 1n'n' 2
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/graph00.ps, 19961211 gbcxx(b)c'fdxx(f)c'fdxx(f)c'fdxx(f)c'fdxx(f)c'fdxx(f)c'fdxx(f)cxp xc'xp xc'xp xc'xp xc'xp xc'xp xc'x
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-351/ECS-LFCS-96-351.ps, 19961211 The Theory of Interacting Deductions and its Application to Operational Semantics Andrew Wilson Doctor of Philosophy University of Edinburgh 1996 i In memory of my father who died after a courageous struggle with a long illness, and to my mother who struggled with him. You taught me faith, hope, love
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/graph0.ps, 19961211 gvbc'fdp wcxxcxxxxc'xgvbfdp wxxx
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/point.ps, 19961211 ca(c)c(2) cca(c) (1) xxx'b(b)(e)(e)e
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/graph01.ps, 19961211 gbcxx(b)c'fdxx(f)c'fdxx(f)c'fdxx(f)c'fdxx(f)c'fdxx(f)c'fdxx(f)cxp xc'xp xc'xp xc'xp xc'xp xc'xp xc'x
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/point2.ps, 19961211 cxa(c)nat nat nat{},y(y)(x)ca,{{(2)cx(c)nat nat nat{},y(y)(x)ccx(c)nat nat nat{},y(y)(x)cnat (y)cca(c)(3)(1)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/multi.ps, 19961211 c(c)w1w2c1c2x1x2y1c(e) e(v)vb(b)x1x2by1c1b(b)x1x2bc2(v)vy1x1(1)c(c)w1w2x1x2y1c(e) ex1(2)ee
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/protocol.ps, 19961211 ,c(c)nat natcc(c)nat cb(b)b(b) ()nat )((e)e(e)e
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/ECS-LFCS-96-350.ps, 19961211 GRAPH TYPES FOR MONADIC MOBILE PROCESSES NOBUKO YOSHIDA Department of Computer Science University of Edinburgh The King's Buildings Mayfield Road Edinburgh, EH9 3JZ, UK e-mail: ny@dcs.ed.ac.uk
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-350/FIG/alpha.ps, 19961211 (2)(1) xacb(e)(f)(b)x'xacb(b)(b)x'd(c)dxax'def(3)
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/96/ECS-LFCS-96-342/ECS-LFCS-96-342.ps, 19961213 ALGEBRAIC STRUCTURE FOR BICATEGORY ENRICHED CATEGORIES R. Gordon and A.J. Power
	ftp://ftp.dcs.ed.ac.uk/pub/lfcsreps/97/ECS-LFCS-97-352/ECS-LFCS-97-352.ps, 19970113 Decidability of Bisimulation Equivalence for Normed Pushdown Processes Colin Stirling Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ, UK email: cps@dcs.ed.ac.uk