**Linear Logic and Petri Nets: Categories, Algebra and Proof**

Carolyn Brown

*LFCS report ECS-LFCS-91-129 (also published as CST-71-91)*

**Semantic Frameworks for Complexity**

Douglas Gurr

*LFCS report ECS-LFCS-91-130 (also published as CST-72-91)*

**Program Specification and Data Refinement in Type Theory**

Zhaohui Luo

*LFCS report ECS-LFCS-91-131*

**Computer Assisted Proof for Mathematics: an Introduction using the LEGO Proof System**

R. Burstall

*LFCS report ECS-LFCS-91-132*

**Deliverables: an approach to program development in the Calculus of Constructions**

Rod Burstall and James McKinna

*LFCS report ECS-LFCS-91-133*

**A Systolizing Compilation Scheme**

C. Lengauer and M. Barnett

*LFCS report ECS-LFCS-91-134*

**Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL**

D. Sannella and B. Kreig-Bruckner

*LFCS report ECS-LFCS-91-135*

**Modal Logics for Mobile Processes**

R. Milner, J. Parrow and D. Walker

*LFCS report ECS-LFCS-91-136*

**The Formalization and Analysis of a Commmunications Protocol**

G. Bruns and S. Anderson

*LFCS report ECS-LFCS-91-137*

**Extended ML: Past, present and future**

D. Sannella and A Tarlecki

*LFCS report ECS-LFCS-91-138*

**A kernel specification formalism with higher-order parameterisation**

D. Sannella and A Tarlecki

*LFCS report ECS-LFCS-91-139*

**Proof Methods and Pragmatics for Parallel Programming**

C. Tofts

*LFCS report ECS-LFCS-91-140 (also published as CST-74-91)*

**Logic Programming: Operational Semantics and Proof Theory**

J Andrews

*LFCS report ECS-LFCS-91-142 (also published as CST-75-91)*

**Relating Processes with Respect to Speed**

F. Moller and C. Tofts

*LFCS report ECS-LFCS-91-143*

**Task Allocation in Monomorphic Ant Species**

C. Tofts

*LFCS report ECS-LFCS-91-144*

**Actions speak louder than words: Proving Bisimilarity for Context-free Processes**

H Huttel and C Stirling

*LFCS report ECS-LFCS-91-145*

**Proof Search in the lambda-Pi-calculus**

David Pym and L Wallen

*LFCS report ECS-LFCS-91-146*

**Correctness-Oriented Approaches to Software Development**

Stephen Gilmore

*LFCS report ECS-LFCS-91-147 (also published as CST-76-91)*

**The Edinburgh SML Library**

Dave Berry

*LFCS report ECS-LFCS-91-148*

**Combinators and Bisimulation Proofs for Restartable Systems**

K V S Prasad

*LFCS report ECS-LFCS-91-149 (also published as CST-77-91)*

**Annotated Transition Systems for Verifying Concurrent Programs**

P. Paczkowski

*LFCS report ECS-LFCS-91-150 (also published as CST-78-91)*

**Tail recursion via universal invariants**

C Barry Jay

*LFCS report ECS-LFCS-91-151*

**The Systematic derivation of Control Signals for Systolic Arrays**

C Lengauer and J Xue

*LFCS report ECS-LFCS-91-152*

**An Improved Systolic Array for String Correction**

C Lengauer and D Sangiorgi

*LFCS report ECS-LFCS-91-153*

**A Unifying theory of Dependent Types I**

Z. Luo

*LFCS report ECS-LFCS-91-154*

**Embedding a CHDDL in a Proof System**

K. Goossens

*LFCS report ECS-LFCS-91-155*

**The Synthesis of Control Signals for One-Dimensional Systolic Arrays**

J Xue and C Lengauer

*LFCS report ECS-LFCS-91-156*

**Modal and Temporal Logics**

Colin Stirling

*LFCS report ECS-LFCS-91-157*

**Logic Programming in a Fragment of Intuitionistic Linear Logic; Extended Abstract**

D Miller and J Hodas

*LFCS report ECS-LFCS-91-158*

**A Logic Programming Language with Lambda-Abstraction, Function Variables and Simple Unification**

D Miller

*LFCS report ECS-LFCS-91-159*

**Unification of Simply Typed Lambda-Terms as Logic Programming**

D Miller

*LFCS report ECS-LFCS-91-160*

**Proof Nets for Multiplicative and Additive Linear Logic**

G Bellin

*LFCS report ECS-LFCS-91-161*

**A Framework for Defining Logics**

Robert Harper, Furio Honsell and Gordon Plotkin

*LFCS report ECS-LFCS-91-162*

**Generating Program Animators from Programming Language Semantics**

D. Berry

*LFCS report ECS-LFCS-91-163 (also published as CST-79-91)*

**An Analysis of a Monte Carlo Algorithm for Estimating the Permanent**

M. Jerrum

*LFCS report ECS-LFCS-91-164*

**Mechanizing Proof Theory: Resource-Aware Logics and Proof-Transformations to extract implicit information**

G. Bellin

*LFCS report ECS-LFCS-91-165 (also published as CST-80-91)*

**Classes of Systolic Y-Tree Automata and a Comparison with Systolic trellis Automata**

Sangiorgi, Fachini and Schettina

*LFCS report ECS-LFCS-91-166*

**A Decision Procedure Revisited: Notes on Direct Logic, Linear Logic and its Implementations**

G Bellin and J Ketonen

*LFCS report ECS-LFCS-91-167*

**The Uniform Proof-theoretic Foundation of Linear Logic Programming (Extended Abstract)**

J Harland and D Pym

*LFCS report ECS-LFCS-91-168*

**Undecidable Equivalences for Basic Process Algebra**

J F Groote and H Huttel

*LFCS report ECS-LFCS-91-169*

**On Hereditary Harrop Formulae as a Basis for Logic Programming**

J Harland

*LFCS report ECS-LFCS-91-170 (also published as CST-81-91)*

**Domain Theory in Realizability Toposes**

Wesley Phoa

*LFCS report ECS-LFCS-91-171 (also published as CST-82-91)*

**Verifying Temporal Properties of Systems with Applications to Petri Nets**

Julian C Bradfield

*LFCS report ECS-LFCS-91-172 (also published as CST-83-91)*

**Silence is Golden: Branching Bisimilarity is Decidable for Context-free Processes**

Hans Huttel

*LFCS report ECS-LFCS-91-173*

**A Distributed Concurrent Implementation of Standard ML**

D. Matthews

*LFCS report ECS-LFCS-91-174*

**A Language for value-passing CCS**

Glenn Bruns

*LFCS report ECS-LFCS-91-175*

**Recent Developments in Systolic Design**

C. Lengauer and J. Xue

*LFCS report ECS-LFCS-91-176*

**Modularizing the Specification of a Small Database System in Extended ML**

E. Kazmierczak

*LFCS report ECS-LFCS-91-177*

**Improved bounds for mixing rates of Markov chains and multicommodity flow**

Alistair Sinclair

*LFCS report ECS-LFCS-91-178*

**A Mildly Exponential Approximation Algorithm for the Permanent**

M. Jerrum

*LFCS report ECS-LFCS-91-179*

**The Polyadic pi-Calculus: A Tutorial**

Robin Milner

*LFCS report ECS-LFCS-91-180*

**Coherence in Category Theory and the Church-Rosser Property**

C B Jay

*LFCS report ECS-LFCS-91-181*

**Fixpoint and Loop Constructions as Colimits**

C B Jay

*LFCS report ECS-LFCS-91-182*

**Long Bn Normal Forms and Confluence**

C B Jay

*LFCS report ECS-LFCS-91-183*

**An Interleaving Model for Real-Time Systems**

Chen Liang

*LFCS report ECS-LFCS-91-184*

**Decidability and Completeness in Real-Time Processes**

Chen Liang

*LFCS report ECS-LFCS-91-185*

**Modelling British Rail's Interlocking Logic: Geographic Data Correctness**

M Morley

*LFCS report ECS-LFCS-91-186*

**Modelling Reduction in Confluent Categories**

C B Jay

*LFCS report ECS-LFCS-91-187*

**An Ideal Model for an Extended Lambda-Calculus with Refinement**

J Agusti et al

*LFCS report ECS-LFCS-91-188*

**The Lazy Lambda Calculus in a Concurrency Scenario**

D Sangiorgi

*LFCS report ECS-LFCS-91-189*

**An n-Categorical Pasting Theorem**

J Power

*LFCS report ECS-LFCS-91-190*

**Decidability, Behavioural Equivalences and Infinite Transition Graphs**

Hans Hüttel

*LFCS report ECS-LFCS-91-191 (also published as CST-86-91)*