View this list backwards.

**1986**-
- Is Computing an Experimental
Science,
*R.Milner* - Standard ML,
*Harper, MacQueen and Milner* - Functor-Category Semantics of
Programming Languages and Logics,
*R. Tennent* - Context-Dependent Bisimulation
between Processes,
*K. Larsen* - Semantical Analysis of Specification
Logic,
*R.Tennent* - Quantification in Algol-like
Languages,
*R.Tennent* - A Calculus of Communicating
Systems,
*R.Milner* - A Complete Axiomatisation for
Observational Congruence of Finite-State Behaviours,
*R.Milner* - Computing with Categories,
*R.Burstall and D.Rydeheard* - A Study in the Foundations of
Programming Methodology: Specifications, Institutions, Charters and
Parchments,
*R.Burstall and J.Goguen* - Modules and Persistence in Standard
ML,
*R.Harper* - Research in Interactive Theorem
Proving at Edinburgh University,
*R.Burstall* - A Complete Protocol Verification
using Relativized Bisimulation,
*K. Larsen and R. Milner* - Introduction to Standard ML,
*R.Harper* - Formal Specification of ML
Programs,
*D.Sannella* - Extended ML: An
institution-independent framework for formal program
development,
*D.Sannella and A.Tarlecki* - Toward formal development of
programs from algebraic specifications: implementations
revisited,
*D.Sannella and A.Tarlecki* - Verifying a CSMA/CD-protocol with
CCS,
*J. Parrow* - Data Abstraction and the
Correctness of Modular Programming,
*O.Schoett* - Gentzenizing Schroeder-Heister's
Natural extension of natural deduction,
*A. Avron* - Some thoughts on algebraic
specification,
*D.Sannella and A.Tarlecki* - Introduction to a Calculus of
Communicating Systems,
*D. Walker*

- Is Computing an Experimental
Science,
**1987**-
- A Framework for Defining
Logics,
*R.Harper, F.Honsell and G.Plotkin* - Comparing Linear and Branching Time
Temporal Logics,
*C. Stirling* - Inductively Defined Functions in
Functional Programming Languages,
*R. Burstall* - Submodule Construction as Equation
Solving in CCS,
*J. Parrow* - The Semantics and Proof Theory of
Linear Logic,
*A. Avron* - A Type Discipline for Program
Modules,
*R.Harper, R.Milner and M.Tofte* - Bisimulation equivalence and
divergence in CCS,
*D. Walker* - Simple Consequence Relations,
*A. Avron* - Using Typed Lambda Calculus to
Implement Formal Systems on a Machine,
*Avron, Honsell and Mason* - Hoare's Logic in the LF,
*I. Mason* - Changes to the Standard ML Core
Language,
*R. Milner* - An Environment for Formal
Systems,
*T G Griffin* - Synchronisation Flow Algebra,
*J Parrow* - The Semantics of Standard ML -
Version 1,
*Harper, Milner, Tofte* - The Generation of Concurrent Code
for Declarative Languages,
*N. Rothwell* - A Categorical Programming
Language,
*T. Hagino* - Theories of translation correctness
for concurrent programming language,
*M. Millington* - Verification of Programs that
Destructively Manipulate Data,
*I. Mason* - Fifth Workshop on Specification of
Abstract Data Types,
*D. Sannella* - The Essence of ML,
*R. Harper and J. Mitchell* - Relative Completeness in Algebraic
Specification,
*Lin Huimin*

- A Framework for Defining
Logics,
**1988**-
- A Typed Lambda Calculus with
Categorical Type Constructors,
*T Hagino* - Analysing mutual exclusion
algorithms using CCS,
*D Walker* - Operational and Algebraic Semantics
of Concurrent Processes,
*R Milner* - Models of Self-Descriptive Set
Theories,
*F Honsell* - Foundations and Proof Theory of
3-valued Logics,
*A.Avron* - Temporal Ordering for
Concurrency,
*C. Tofts* - How to Breed
Compiler/Interpreters,
*A. Gordon* - Bisimulations for Concurrency,
*I. Castellani* - Workshop on General Logic -
Edinburgh 1987,
*Avron, Harper, Honsell, Mason and Plotkin* - On Functors Expressible in the
Polymorphic Typed Lambda Calculus,
*J. Reynolds and G. Plotkin* - Operational Semantics and
Polymorphic Type Inference,
*Mads Tofte* - Unifying Exceptions with
Constructors in Standard ML,
*Milner, Tofte, MacQueen, Appel* - A Survey of Formal Software
Development Methods,
*D. Sannella* - A Higher-order Calculus and Theory
Abstraction,
*Zhaohui Luo* - CC and its Meta Theory,
*Zhaohui Luo* - Constructing Type Systems over an
Operational Semantics,
*R. Harper* - Some Fundamental Algebraic Tools
for the Semantics of Computation - Part III: Indexed
Categories,
*A Tarlecki, R M Burstall and J A Goguen* - The Interactive Proof Editor - An
Experiment in Interactive Theorem,
*B Ritchie and P Taylor* - The Definition of Standard ML -
Version 2,
*R Harper, R Milner and M Tofte* - The Partial Lambda-Calculus,
*E. Moggi* - E.U. Postgraduate Exam Questions in
Computation Theory,
*D. Sannella* - Co-Induction in Relational
Semantics,
*R. Milner and M. Tofte* - Computational Lambda-Calculus and
Monads,
*E. Moggi* - An Equational Formulation of
LF,
*R. Harper* - The Design and Implementation of an
Interactive Proof Editor,
*B. Ritchie* - A Natural Deduction treatment of
Operational Semantics,
*R Burstall and F. Honsell*

- A Typed Lambda Calculus with
Categorical Type Constructors,
**1989**-
- Using Constructions as a
Metalanguage,
*Paul Taylor* - Towards formal development of ML
programs, foundations and methodology,
*Donald Sannella and Andrzej Tarlecki* - Proving correctness of constructor
implementations,
*Jorge Farrés-Casals* - Four Lectures on Standard ML,
*Mads Tofte* - THORN: A Theorem-Prover that
compiles first-order Logic into LISP,
*M. Tarver* - Structure and Representation in
LF,
*Harper, Sannella and Tarlecki* - Characteristic Formulae for CCS
with Divergence,
*B. Steffen* - Proof-Theoretic Characterisations
of Logic Programming,
*J. Andrews* - Local Model Checking in the Modal
Mu-Calculus,
*C. Stirling and D. Walker* - Finite Constants: Characterizations
of a new decidable set of constants,
*B. Steffen and J. Knoop* - DIALOG: A Theorem-proving
environment designed to unify Functional and Logic Programming,
*M. Tarver* - The Definition of Standard ML -
Version 3,
*Harper, Milner and Tofte* - Optimal Data Flow Analysis via
Observational Equivalence,
*Bernhard Steffen* - The Concurrency Workbench: A
Semantics-based Verification Tool for Finite-State Systems,
*R. Cleaveland, J. Parrow and B. Steffen* - Axioms for Concurrency,
*Faron Moller* - A Calculus of Mobile Processes
Pt.1,
*Milner, Parrow and Walker* - A Calculus of Mobile Processes
Pt.2,
*Milner, Parrow and Walker* - Relating Petri Nets to Formulae of
Linear Logic,
*Carolyn Brown* - On Natural deduction style
semantics, environments and stores,
*Christian-Emil Ore* - Playing with Lego: Some examples of
developing mathematics in the Calculus of Constructions,
*Paul Taylor* - Some Fundamental Algebraic Tools
for the Semantics of Computation. Part 3. Indexed Categories,
*R. Burstall, J. Goguen and A. Tarlecki* - Automated Analysis of Mutual
Exclusion Algorithms using CCS,
*D J Walker* - The Structure of free closed
categories,
*C Barry Jay* - Equations, dependent equations and
quasi-dependent equations -- on their unification,
*Sun Yong* - Equational Characterization of
Binding (Extended Abstract),
*Sun Yong* - Logical Design of VLSI Circuit with
Extension of Uncertainty (or monotonic functional completeness of
Kleene ternary logic),
*Sun Yong* - Petri Nets as Quantales,
*Carolyn Brown* - The Nonexistence of Finite
Axiomatisations for CCS congruences,
*Faron Moller* - Self-independent Petri Nets (or a
dead-lock-free paradigm),
*Sun Yong* - Compositional Characterization of
observable Program Properties,
*B. Steffen, C.B. Jay, M. Mendler* - Proving total correctness of
concurrent programs without using auxiliary variables,
*P. Paczkowski* - Syntax, typechecking and Dynamic
Semantics for Extended ML,
*D. Sannella and F. da Silva* - Formal program development in
Extended ML for the working programmer,
*D. Sannella* - Timing Concurrent Processes,
*C. Tofts* - A Temporal Calculus of
Communicating Systems,
*Faron Moller and Chris Tofts*

- Using Constructions as a
Metalanguage,
**1990**-
- Probabilistic Non-Determinism,
*Claire Jones* - INSTITUTIONS: Abstract Model
Theory for Specification and Programming,
*R. Burstall and J. Goguen* - Extending properties to categories
of partial maps,
*C. Barry Jay* - Relative Frequency in a
Synchronous Calculus,
*Chris Tofts* - Tactics for State Space Reduction
on the Concurrency Workbench,
*M.J. Morley* - The Logical Structure of
Sequential Prolog,
*J. Andrews* - Investigations into proof-search
in a system of first-order dependent function types,
*D. Pym and L. Wallen* - Higher-Order Modules and the Phase
Distinction,
*Harper, Moggi and Mitchell* - An Abstract View of Programming
Languages,
*E. Moggi* - A Systolic Array for Pyramidal
Algorithms,
*C. Lengauer and J. Xue* - Local Model Checking for Infinite
State Spaces,
*Julian Bradfield and Colin Stirling* - On the Description and Development
of One-Dimensional Systolic Arrays,
*C Lengauer and J. Xue* - Proving correctness w.r.t.
specifications with hidden parts,
*Jorge Farrés-Casals* - An Extended Calculus of
Constructions,
*Zhaohui Luo* - Relevance Logic and Concurrent
Composition,
*Mads Dam* - Constructive lambda-Models,
*Andreas Knobel* - A Problem of Adequacy:
conservativity of calculus of constructions over higher-order
logic,
*Zhaohui Luo* - pi-calculus Semantics of
Object-Oriented Programming Languages,
*David Walker* - Translating CTL* into the modal
mu-calculus,
*Mads Dam* - The Uniform Proof-Theoretic
Foundation of Linear Logic Programming,
*James Harland and David Pym* - Proofs, Search and Computation in
General Logic,
*David Pym* - Towards a Formal Framework for
Evaluation of Operational Semantics Specifications,
*Fabio da Silva* - A Timed Calculus of Communicating
Systems,
*Liang Chen, Stuart Anderson and Faron Moller* - The Autosynchronisation of
Leptothorax Acervorum (Fabricius) described in WSCCS,
*Chris Tofts*

- Probabilistic Non-Determinism,
**1991**-
- Linear Logic and Petri Nets:
Categories, Algebra and Proof,
*Carolyn Brown* - Semantic Frameworks for
Complexity,
*Douglas Gurr* - Program Specification and Data
Refinement in Type Theory,
*Zhaohui Luo* - Computer Assisted Proof for
Mathematics: an Introduction using the LEGO Proof System,
*R. Burstall* - Deliverables: an approach to
program development in the Calculus of Constructions,
*Rod Burstall and James McKinna* - A Systolizing Compilation
Scheme,
*C. Lengauer and M. Barnett* - Structuring Specifications
in-the-Large and in-the-Small: Higher-Order Functions, Dependent
Types and Inheritance in SPECTRAL,
*D. Sannella and B. Kreig-Bruckner* - Modal Logics for Mobile
Processes,
*R. Milner, J. Parrow and D. Walker* - The Formalization and Analysis of
a Commmunications Protocol,
*G. Bruns and S. Anderson* - Extended ML: Past, present and
future,
*D. Sannella and A Tarlecki* - A kernel specification formalism
with higher-order parameterisation,
*D. Sannella and A Tarlecki* - Proof Methods and Pragmatics for
Parallel Programming,
*C. Tofts* - Logic Programming: Operational
Semantics and Proof Theory,
*J Andrews* - Relating Processes with Respect to
Speed,
*F. Moller and C. Tofts* - Task Allocation in Monomorphic Ant
Species,
*C. Tofts* - Actions speak louder than words:
Proving Bisimilarity for Context-free Processes,
*H Huttel and C Stirling* - Proof Search in the
lambda-Pi-calculus,
*David Pym and L Wallen* - Correctness-Oriented Approaches to
Software Development,
*Stephen Gilmore* - The Edinburgh SML Library,
*Dave Berry* - Combinators and Bisimulation
Proofs for Restartable Systems,
*K V S Prasad* - Annotated Transition Systems for
Verifying Concurrent Programs,
*P. Paczkowski* - Tail recursion via universal
invariants,
*C Barry Jay* - The Systematic derivation of
Control Signals for Systolic Arrays,
*C Lengauer and J Xue* - An Improved Systolic Array for
String Correction,
*C Lengauer and D Sangiorgi* - A Unifying theory of Dependent
Types I,
*Z. Luo* - Embedding a CHDDL in a Proof
System,
*K. Goossens* - The Synthesis of Control Signals
for One-Dimensional Systolic Arrays,
*J Xue and C Lengauer* - Modal and Temporal Logics,
*Colin Stirling* - Logic Programming in a Fragment of
Intuitionistic Linear Logic; Extended Abstract,
*D Miller and J Hodas* - A Logic Programming Language with
Lambda-Abstraction, Function Variables and Simple Unification,
*D Miller* - Unification of Simply Typed
Lambda-Terms as Logic Programming,
*D Miller* - Proof Nets for Multiplicative and
Additive Linear Logic,
*G Bellin* - A Framework for Defining
Logics,
*Robert Harper, Furio Honsell and Gordon Plotkin* - Generating Program Animators from
Programming Language Semantics,
*D. Berry* - An Analysis of a Monte Carlo
Algorithm for Estimating the Permanent,
*M. Jerrum* - Mechanizing Proof Theory:
Resource-Aware Logics and Proof-Transformations to extract implicit
information,
*G. Bellin* - Classes of Systolic Y-Tree
Automata and a Comparison with Systolic trellis Automata,
*Sangiorgi, Fachini and Schettina* - A Decision Procedure Revisited:
Notes on Direct Logic, Linear Logic and its Implementations,
*G Bellin and J Ketonen* - The Uniform Proof-theoretic
Foundation of Linear Logic Programming (Extended Abstract),
*J Harland and D Pym* - Undecidable Equivalences for Basic
Process Algebra,
*J F Groote and H Huttel* - On Hereditary Harrop Formulae as a
Basis for Logic Programming,
*J Harland* - Domain Theory in Realizability
Toposes,
*Wesley Phoa* - Verifying Temporal Properties of
Systems with Applications to Petri Nets,
*Julian C Bradfield* - Silence is Golden: Branching
Bisimilarity is Decidable for Context-free Processes,
*Hans Huttel* - A Distributed Concurrent
Implementation of Standard ML,
*D. Matthews* - A Language for value-passing
CCS,
*Glenn Bruns* - Recent Developments in Systolic
Design,
*C. Lengauer and J. Xue* - Modularizing the Specification of
a Small Database System in Extended ML,
*E. Kazmierczak* - Improved bounds for mixing rates
of Markov chains and multicommodity flow,
*Alistair Sinclair* - A Mildly Exponential Approximation
Algorithm for the Permanent,
*M. Jerrum* - The Polyadic pi-Calculus: A
Tutorial,
*Robin Milner* - Coherence in Category Theory and
the Church-Rosser Property,
*C B Jay* - Fixpoint and Loop Constructions as
Colimits,
*C B Jay* - Long Bn Normal Forms and
Confluence,
*C B Jay* - An Interleaving Model for
Real-Time Systems,
*Chen Liang* - Decidability and Completeness in
Real-Time Processes,
*Chen Liang* - Modelling British Rail's
Interlocking Logic: Geographic Data Correctness,
*M Morley* - Modelling Reduction in Confluent
Categories,
*C B Jay* - An Ideal Model for an Extended
Lambda-Calculus with Refinement,
*J Agusti et al* - The Lazy Lambda Calculus in a
Concurrency Scenario,
*D Sangiorgi* - An n-Categorical Pasting
Theorem,
*J Power* - Decidability, Behavioural
Equivalences and Infinite Transition Graphs,
*Hans Hüttel*

- Linear Logic and Petri Nets:
Categories, Algebra and Proof,
**1992**-
- Semantics of Local Variables,
*R D Tennent and O'Hearn* - Verification of Parallel Systems
via Decomposition,
*J F Groote and F Moller* - First Order Linear Logic in
Symmetric Monoidal Closed Categories,
*Simon Ambler* - Formal Program Development in
Modular Prolog: A Case Study,
*M Read and E Kazmierczak* - Ordinal Complexity of Recursive
Programs and their Termination Proofs,
*M Fairtlough* - Loop Parallelization and
Unimodularity,
*C. Lengauer and M. Barnett* - Efficient Algorithms for Listing
Combinatorial Structures,
*Leslie Ann Goldberg* - A Proof Assistant for Symbolic
Model-Checking,
*J C Bradfield* - Intersection Types and Bounded
Polymorphism,
*Benjamin Pierce* - Approximating the Permanent: a
Simple Approach,
*L E Rasmussen* - A Unifying Theory of Dependent
Types: the Schematic Approach,
*Zhaohui Luo* - The Formal Synthesis of Control
Signals for Systolic Arrays,
*Jingling Xue* - Toward Formal Development of
Programs from Algebraic Specifications: Model-Theoretic
Foundations,
*D. Sannella and A Tarlecki* - Tail Recursion through Universal
Invariants,
*C B Jay* - A Set-theoretic Setting for
Structuring Theories in Proof Development,
*Z. Luo and R. Burstall* - A Framework for Binding
Operators,
*Sun Yong* - An introduction to fibrations,
topos theory, the effective topos and modest sets,
*Wesley Phoa* - Inductive Data Types:
Well-ordering Types Revisited,
*H. Goguen and Zhaohui Luo* - Listing Graphs that Satisfy First
Order Sentences,
*L A Goldberg* - LEGO Proof Development System:
User's Manual,
*Zhaohui Luo and R Pollack* - On Resolution in Fragments of
Classical Linear Logic (Extended Abstract),
*J Harland and D J Pym* - A proposed categorical semantics
for Pure ML,
*Wesley Phoa and Michael Fourman* - From term models to domains,
*Wesley Phoa* - Building domains from graph
models,
*Wesley Phoa* - Process-Algebraic Interpretations
of Positive Linear and Relevant Logics,
*Mads Dam* - CTL* and ECTL* as fragments of the
modal mu-calculus,
*Mads Dam* - Bisimulation Equivalence is
Decidable for all Context-Free Processes,
*Soren Christensen, Hans Hüttel, Colin Stirling* - Unlimp - Uniqueness as a Leitmotiv
for Implementation,
*Stefan Kahrs* - Verification in ASL and related
specification languages,
*Jorge Farrés-Casals* - Modal and Temporal Logics for
Processes,
*Colin Stirling* - Toward formal development of
programs from algebraic specifications: parameterisation
revisited,
*Donald Sannella, Stefan Sokolowski and Andrzej Tarlecki* - Relational Parametricity and Local
Variables,
*P W O'Hearn and R D Tennent* - Fixpoints of Büchi
automata,
*Mads Dam* - Object-Oriented Programming
Without Recursive Types,
*Benjamin C Pierce and David N Turner* - An Abstract View of Objects and
Subtyping ,
*Martin Hofmann and Benjamin C Pierce* - Representing Logics in Type
Theory,
*Philippa Gardner* - Formal Development of Functional
Programs in Type Theory - A Case Study,
*Martin Hofmann* - A Unification Algorithm for the
lambda-Pi-Calculus,
*David Pym* - Brewing Strong Normalization
Proofs with LEGO,
*Thorsten Altenkirch* - Opeerational Semantics Based
Formal Symbolic Simulation,
*K G W Goossens* - On the pi-Calculus and Linear
Logic,
*G Bellin and P J Scott* - Correctness Proofs of Compilers
and Debuggers: an Overview of an Approach Based on Structural
Operational Semantics,
*Fabio Q B da Silva* - A Sub-logarithmic Communication
Algorithm for the Completely Connected Optical Communication
Parallel Computer,
*Leslie Ann Goldberg and Mark Jerrum* - Functional Compilation from the
Standard ML Core Language to Lambda Calculus,
*Nick Rothwell* - Parsing in the SML Kit,
*Nick Rothwell* - Miscellaneous Design Issues in the
ML Kit,
*Nick Rothwell* - Polymorphic Type Checking by
Interpretation of Code,
*Stefan Kahrs* - A Case Study in Safety-Critical
Design,
*Glenn Bruns* - Observational Equivaalence and
Compiler Correctness,
*Fabio Q B da Silva* - Correctness Proofs of Compilers
and Debuggers: an Approach Based on Structural Operational
Semantics,
*Fabio Q B da Silva* - Deliverables: a categorical
approach to program development in type theory,
*Rod Burstall and James McKinna* - The Virtues of Eta-expansion,
*C Barry Jay and Neil Ghani* - Decomposability, Decidability and
Axiomatisability for Bisimulation Equivalence on Basic Parallel
Processes,
*S Christensen, Y Hirshfield and F Moller* - A Semantics for Static Type
Inference,
*Gordon Plotkin* - Logic Programming via Proof-Valued
Computations,
*David J Pym and Lincoln A Wallen* - Deliverables: a categorical
approach to program development in type theory,
*James Hugh McKinna* - A Synopsis on the Identification
of Linear Logic Programming Languages,
*James Harland and David Pym* - Action Structures,
*Robin Milner* - An Algorithm for Constructing
beta-eta-long normal forms,
*Philippa Gardner* - Equivalences between Logics and
their Representing Type Theories,
*Philippa Gardner* - Newtonian Arbiters Cannot be
Proven Correct,
*Michael Mendler and Terry Stroup* - Hiding and Behaviour: An
Institutional Approach,
*Rod Burstall and Razvan Diaconescu*

- Semantics of Local Variables,
**1993**-
- Enrichment Through Variation,
*R. Gordon and A. J. Power* - A Modal Logic for Handling
Behavioural Constraints in Formal Hardware Verification,
*Michael Mendler* - Statically Types Friendly
Functions via Partially Abstract Types,
*B C Pierce and D N Turner* - Mistakes and Ambiguities in the
Definition of Standard ML,
*Stefan Kahrs* - PAC-Learning Geometrical
Figures,
*Paul W Goldberg* - Approximately Counting Hamilton
Cycles in Dense Graphs,
*Martin Dyer, Alan Frieze and Mark Jerrum* - Simulated Annealing for Graph
Bisection,
*Mark Jerrum and Gregory Sorkin* - Decidability Questions for
Bisimilarity of Petri Nets and Some Related Problems,
*Petr Jancar* - Algebraic Theories for
Name-Passing Calculi,
*Joachim Parrow and Davide Sangiorgi* - Literate Programming: A
Review,
*Angus Duggan* - Action Structures for the
pi-Calculus,
*Robin Milner* - Errata and Remarks,
*David J Pym* - Expressing Mobility in Process
Algebras: First-Order and Higher-Order Paradigms,
*Davide Sangiorgi* - Correctness of Data
Representations in Algol-like Languages,
*R D Tennent* - Embedding Hardware Description
Languages in Proof Systems,
*Kees G W Goossens* - The Formalisation of a Hardware
Description Language in a Proof System: Motivation and
Applications,
*Kees G W Goossens* - A Theory of Bisimulation for the
pi-calculus,
*Davide Sangiorgi* - Timed Processes: Models, Axioms
and Decidability,
*Liang Chen* - Uniform sampling modulo a group of
symmetries using Markov chain simulation,
*Mark Jerrum* - Structure and Behaviour in
Hardware Verification,
*K G W Goossens* - On the decidability of model
checking for several mu-calculi and Petri Nets,
*Javier Esparza* - Multiple Inheritance via
Intersection Types,
*Adriana B Compagnoni and Benjamin C Pierce* - Undecidable Equivalences for Basic
Parallel Processes,
*Hans Hüttel* - Fibrations, Logical Predicates and
Indeterminates,
*Claudio Alberto Hermida* - Decidability and Decomposition in
Process Algebras,
*Soren Christensen* - Constructions, Inductive Types and
Strong Normalization,
*Thorsten Altenkirch*

- Enrichment Through Variation,
**1994**-
- Higher-Order Subtyping,
*Martin Steffen and Benjamin Pierce* - Subtyping in F-omega-Meet is
decidable,
*Adriana B Compagnoni* - Locality and Non-interleaving
Semantics in calculi for mobile processes,
*Davide Sangiorgi* - Interfaces and Extended ML,
*Stefan Kahrs, Donald Sannella and Andrzej Tarlecki* - First-Class Polymorphism for
ML,
*Stefan Kahrs* - The Mobility Workbench. A tool for
the pi-Calculus,
*Björn Victor and Faron Moller* - A polynomial algorithm for
deciding bisimilarity of normed context-free processes,
*Yoram Hirshfeld, Mark Jerrum and Faron Moller* - Applying Process Refinement to a
Safety-Relevant System,
*Glenn Bruns* - A polynomial-time algorithm for
deciding bisimulation equivalence of normed Basic Parallel
Processes,
*Yoram Hirshfeld, Mark Jerrum and Faron Moller* - Why tricategories?,
*A J Power* - A very simple algorithm for
estimating the number of k-colourings of a low-degree graph,
*Mark Jerrum* - Congruences in Commutative
Semigroups,
*Yoram Hirshfeld* - Improved approximation algorithms
for MAX k-CUT and MAX BISECTION,
*Alan Frieze and Mark Jerrum* - On modal mu-calculus and
Büchi tree automata,
*Roope Kaivola* - Deciding equivalences in simple
Process Algebras,
*Yoram Hirshfeld* - Trapping Mutual Exclusion in the
Box Calculus,
*Javier Esparza and Glenn Bruns* - The Computational Complexity of
Counting,
*Mark Jerrum* - A fully abstract semantics for
causality in the pi-calculus,
*Michele Boreale and Davide Sangiorgi* - High Undecidability of Weak
Bisimilarity for Petri Nets,
*Petr Jancar* - On the Bisimulation Proof
Method,
*Davide Sangiorgi* - The Definition of Extended ML,
*Stefan Kahrs, Donald Sannella, Andrzej Tarlecki* - An Old Sub-Quadratic Algorithm for
Finding Extremal Sets,
*Paul Pritchard* - Decidability of Model Checking for
Infinite-State Concurrent Systems,
*Javier Esparza* - Positive Subtyping,
*Martin Hofmann and Benjamin Pierce* - A Typed Operational Semantics for
Type Theory,
*Healfdene Goguen* - Balancing Load under Large and
Fast Load Changes in Distributed Computing Systems,
*Thierry Le Sergent and Bernard Berthomieu* - Adaptive selection of protocols
for strict coherency in distributed shared memory,
*Thierry Le Sergent and David C J Matthews* - Axiomatic Domain Theory in
Categories of Partial Maps,
*Marcelo P. Fiore* - The Proof Theory and Semantics of
Intuitionistic Modal Logic,
*Alex K. Simpson* - On Computing the Subset Graph of a
Collection of Sets,
*Paul Pritchard* - Supporting Formal Reasoning about
Standard ML,
*Graham Collins and Stephen Gilmore* - Concurrency in a Natural
Semantics,
*Kevin Mitchell* - Multiple Values in Standard
ML,
*Kevin Mitchell* - Generating and counting Hamilton
cycles in random regular graphs,
*Alan Frieze, Mark Jerrum, Michael Molloy, Robert Robinson and Nicholas Wormald*

- Higher-Order Subtyping,
**1995**-
- Towards a Domain Theory for
Termination Proofs,
*Stefan Kahrs* - Correct Separate and Selective
Closure Conversion,
*Paul Steckler* - LEMMA Interface Definition,
*David C J Matthews and Thierry Le Sergent* - Computational Pólya
Theory,
*Mark Jerrum* - On behavioural abstraction and
behavioural satisfaction in higher-order logic,
*Martin Hofmann and Donald Sannella* - Proof and Design,
*Michael P. Fourman* - Typing Abstract Data Types,
*Judith Underwood* - Tableau for Intuitionistic
Predicate Logic as Metatheory,
*Judith Underwood* - The definition of Extended ML: a
gentle introduction,
*Stefan Kahrs, Donald Sannella and Andrzej Tarlecki* - The Theory of LEGO,
*Robert Pollack* - Axiomatising Linear Time
Mu-calculus,
*Roope Kaivola* - LEMMA: A Distributed Shared Memory
with Global and Local Garbage Collection,
*David C J Matthews and Thierry Le Sergent* - A quasi-polynomial-time algorithm
for sampling words from a context-free language,
*Vivek Gore and Mark Jerrum* - Extensional concepts in
intensional type theory,
*Martin Hofmann* - The Algebra of Finite State
Processes,
*Peter Michael Sewell* - Formal Derivation of a Class of
Computers,
*Li-Guo Wang* - Lax naturality through
enrichment,
*Yoshiki Kinoshita and John Power* - First Steps on the Representation
of Domains,
*Marcelo P Fiore* - Realizability Toposes and Language
Semantics,
*John R. Longley* - Formal Design of a Class of
Computers,
*Li-Guo Wang and Michael Mendler* - Abstraction of Hardware
Construction,
*Li-Guo Wang and Michael Mendler* - Papers on Poly/ML,
*David C J Matthews* - Universal Structure and a
Categorical Framework for Type Theory,
*Makoto Takeyama* - An effective tableau system for
the linear time mu-calculus,
*Julian Bradfield, Javier Esparza and Angelika Mader* - On the expressivity of the modal
mu-calculus,
*Julian Bradfield* - Adjoint rewriting,
*Neil Ghani*

- Towards a Domain Theory for
Termination Proofs,
**1996**-
- Detecting Local Channels in
Distributed Poly/ML,
*Paul Steckler* - Partial Functions in a Total
Setting,
*Simon Finn, Michael Fourman and John Longley* - Algebraic Structure for Bicategory
Enriched Categories,
*R Gordon and A J Power* - A New Approach to Polynomial-time
Generation of Random Points in Convex Bodies,
*Russ Bubley, Martin Dyer and Mark Jerrum* - Standard ML Type Generativity as
Existential Quantification,
*Claudio Russo* - The Polymorphic Pi-Calculus:
Theory and Implementation,
*David Turner* - Computational applications of
calculi based on monads,
*Pietro Cenciarelli* - Dual Intuitionistic Linear
Logic,
*Andrew Barber* - Safety Assurance in Interlocking
Design,
*Matthew John Morley* - The Swendsen-Wang process does not
always mix rapidly,
*Vivek Gore and Mark Jerrum* - Graph Types for Monadic Mobile
Processes,
*Nobuko Yoshida* - The Theory of Interacting
Deductions and its Application to Operational Semantics,
*Andrew Wilson*

- Detecting Local Channels in
Distributed Poly/ML,
**1997**-
- Decidability of Bisimulation
Equivalence for Normed Pushdown Processes,
*Colin Stirling* - Logical Full Abstraction and
PCF,
*John Longley and Gordon Plotkin* - A Type-Theoretic Analysis of
Modular Specifications,
*Savitri Maharaj* - Model Checking the Full Modal
Mu-Calculus for Infinite Sequential Processes,
*Olaf Burkart and Bernhard Steffen* - Using Automata to Characterise
Fixed Point Temporal Logics,
*Roope Kaivola* - Sequent Combinators: A Hilbert
System for the Lambda Calculus,
*Healfdene Goguen* - Candidates for Substitution,
*Healfdene Goguen and James McKinna* - Some Lambda Calculus and Type
Theory Formalized,
*James McKinna and Robert Pollack* - Models of Sharing Graphs: A
Categorical Semantics of let and letrec,
*Masahito Hasegawa* - Typed Operational Semantics for
Higher Order Subtyping,
*Adriana Compagnoni and Healfdene Goguen* - The C-LEMMA Memory Interface on
the Cray T3D,
*Christopher D. Walton and Bruce J. McAdam* - Subject Reduction and Minimal
Types for Higher Order Subtyping,
*Adriana Compagnoni* - Programming in Standard ML '97: A
Tutorial Introduction,
*Stephen Gilmore* - Decidable Higher Order
Subtyping,
*Adriana Compagnoni* - Relative Equational Specification
and Semantics,
*Jo Erskine Hannay* - The modal mu-calculus alternation
hierarchy is strict,
*J.C. Bradfield* - Implementing Proof by Pointing
without a Structure Editor,
*Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira* - The Verification of Asynchronous
Circuits using CCS,
*Graham Clark and George Taylor* - Subtyping Dependent Types,
*David Aspinall and Adriana Compagnoni* - Linear Type Theories, Semantics
and Action Calculi,
*Andrew Barber* - Lecture Notes on Formal Program
Development,
*Stefan Kahrs* - Using Markovian Process Algebra to
Specify Interactions in Queueing Systems,
*Nigel Thomas and Jane Hillston* - PCF extended with real numbers: a
domain-theoretic approach to higher-order exact real number
computation,
*Martín Hötzel Escardó* - That About Wraps it Up: Using FIX
to Handle Errors Without Exceptions, and Other Programming
Tricks,
*Bruce J. McAdam* - Categorical Structure of
Continuation Passing Style,
*Hayo Thielecke* - Elementary structural analysis for
PEPA,
*Stephen Gilmore, Jane Hillston and Laura Recalde* - Dynamic ML without Dynamic
Types,
*Stephen Gilmore, Dilsun Kirli and Christopher Walton* - Machine Assisted Proofs for
Generic Semantics to Compiler Transformation Correctness
Theorems,
*Saif Ullah Kahn*

- Decidability of Bisimulation
Equivalence for Normed Pushdown Processes,
**1998**-
- Process Abstraction in the
Verification of Temporal Properties,
*Glenn R. Bruns* - Notes on Simply Typed Lambda
Calculus,
*Ralph Loader* - A Class of PEPA Models Exhibiting
Product Form Solution over Submodels,
*Jane Hillston* - Injective spaces and the filter
monad,
*Martín Hötzel Escardó* - On the Unification of
Substitutions in Type-Inference,
*Bruce J. McAdam* - Simplifying the modal mu-calculus
alternation hierarchy,
*Julian C. Bradfield* - Bisimulation equivalence is
decidable for normed Process Algebra,
*Yoram Hirshfeld and Mark Jerrum* - The ``Burnside process'' converges
slowly,
*Leslie Ann Goldberg and Mark Jerrum* - A Manufacturing Production Line
with Service Interruptions,
*Nigel Thomas and Isi Mitrani* - Types For Modules,
*Claudio V. Russo* - Applicative Notions in ML-like
Programs,
*Budi Halim Ling* - On counting independent sets in
sparse graphs,
*Martin Dyer, Alan Frieze and Mark Jerrum* - Hoare Logic and VDM:
Machine-Checked Soundness and Completeness Proofs,
*Thomas Kleymann* - Metatheory of Verification Calculi
in LEGO: To What Extent Does Syntax Matter?,
*Thomas Kleymann* - Learning Function Free Horn
Expressions,
*Roni Khardon* - Learning Range Restricted Horn
Expressions,
*Roni Khardon* - Categorical Term Rewriting: Monads
and Modularity,
*Christoph Lüth* - Equivalence semantics for
concurrency: comparison and application,
*Vashti Christina Galpin* - Referential Opacity in Equational
Reasoning,
*Jo Erskine Hannay* - Hoare Logic and Auxiliary
Variables,
*Thomas Kleymann* - Direct models for the
computational lambda-calculus,
*Carsten Führmann* - Nested Sketches,
*Horst Reichel* - The sequentially realizable
functionals,
*John Longley* - Type Inference with Bounded
Quantification,
*Dilip Sequeira*

- Process Abstraction in the
Verification of Temporal Properties,
**1999**-
- Diluting ACID,
*Tim Kempster, Colin Stirling and Peter Thanisch* - Pre-logical Relations,
*Furio Honsell and Donald Sannella* - Type Systems For Polynomial-time
Computation,
*Martin Hofmann* - Architectural Specifications in
CASL,
*Michel Bidoit, Donald Sannella and Andrzej Tarlecki* - Decidability and complexity of
equivalences for simple process algebras,
*Jitka Stríbrná* - A Semantic analysis of
control,
*James David Laird* - Abstract Machines for Memory
Management,
*Christopher Walton* - Decidability of DPDA
equivalence,
*Colin Stirling* - A Theory of Program
Refinement,
*Ewen Denney* - A Polymorphic Type and Effect
System for Detecting Mobile Functions,
*Dilsun Kirli* - Fully Complete Models for ML
Polymorphic Types,
*Samson Abramsky and Marina Lenisa* - Graphs for Recording Type
Information,
*Bruce J. McAdam* - Proving Correctness of Modular
Functional Programs,
*Christopher Owens* - Counting unlabelled subtrees of a
tree is #P-complete,
*Leslie Ann Goldberg and Mark Jerrum*

- Diluting ACID,
**2000**-
- A Type-Based Locality Analysis for a Functional Distributed Language,
*Alvaro Freitas Moreira* - Dependently Typed Functional Programs and their Proofs,
*Conor McBride* - Techniques for the Construction and Analysis of Algebraic Performance Models,
*Graham Clark* - Ordinals and Interactive Programs,
*Peter Hancock* - The structure of call-by-value,
*Carsten Führmann* - Testing from Structured Algebraic Specifications: The Oracle Problem,
*Patricia D. L. Machado* - Exact completions and toposes,
*Matias Menni*

- A Type-Based Locality Analysis for a Functional Distributed Language,
**2001**-
- Abstract Machines for Dynamic Computation,
*Christopher David Walton*

- Abstract Machines for Dynamic Computation,
**2002**-
- Diagrammatic Representations in Domain-Specific Languages,
*Konstantinos Tourlas* - Repairing Type Errors in Functional Programs,
*Bruce James McAdam* - Mobile Computation with Functions,
*Zeliha Dilsun Kirli* - Asynchronous Queue Machines with Explicit Forwarding,
*Lennart Beringer* - Conservative extensions of the lambda-calculus for the computational interpretation of sequent calculus,
*José Carlos Soares do Espírito Santo*

- Diagrammatic Representations in Domain-Specific Languages,
**2003**-
- Games for Modal and Temporal Logics,
*Martin Lange* - Game Semantics and Subtyping,
*Juliusz Chroboczek* - Abstraction Barriers and
Refinement in the Polymorphic Lambda Calculus,
*Jo Erskine Hannay*

- Games for Modal and Temporal Logics,
**2004**-
- Decidability and Coincidence of Equivalences for Concurrency
*Sibylle Fröschle* - Coalgebraic Modelling of Timed Processes
*Marco Kick* - Observational Models of Requirements Evolution
*Massimo Felici* - Towards compositional CSL model-checking
*Paolo Ballarini* - Pseudo-Distributive Laws and a Unified Framework for Variable Binding
*Miki Tanaka*

- Decidability and Coincidence of Equivalences for Concurrency