All LFCS reports

View this list backwards.

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

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

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

2001

• Abstract Machines for Dynamic Computation, Christopher David Walton

2000

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

1999

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

1998

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

1997

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

1996

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

1995

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

1994

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

1993

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

1992

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

1991

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

1990

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

1989

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

1988

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

1987

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

1986

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