**Semantics of Local Variables**

R D Tennent and O'Hearn

*LFCS report ECS-LFCS-92-192*

**Verification of Parallel Systems via Decomposition**

J F Groote and F Moller

*LFCS report ECS-LFCS-92-193*

**First Order Linear Logic in Symmetric Monoidal Closed Categories**

Simon Ambler

*LFCS report ECS-LFCS-92-194 (also published as CST-87-92)*

**Formal Program Development in Modular Prolog: A Case Study**

M Read and E Kazmierczak

*LFCS report ECS-LFCS-92-195*

**Ordinal Complexity of Recursive Programs and their Termination Proofs**

M Fairtlough

*LFCS report ECS-LFCS-92-196 (also published as CST-88-92)*

**Loop Parallelization and Unimodularity**

C. Lengauer and M. Barnett

*LFCS report ECS-LFCS-92-197*

**Efficient Algorithms for Listing Combinatorial Structures**

Leslie Ann Goldberg

*LFCS report ECS-LFCS-92-198 (also published as CST-89-92)*

**A Proof Assistant for Symbolic Model-Checking**

J C Bradfield

*LFCS report ECS-LFCS-92-199*

**Intersection Types and Bounded Polymorphism**

Benjamin Pierce

*LFCS report ECS-LFCS-92-200*

**Approximating the Permanent: a Simple Approach**

L E Rasmussen

*LFCS report ECS-LFCS-92-201*

**A Unifying Theory of Dependent Types: the Schematic Approach**

Zhaohui Luo

*LFCS report ECS-LFCS-92-202*

**The Formal Synthesis of Control Signals for Systolic Arrays**

Jingling Xue

*LFCS report ECS-LFCS-92-203 (also published as CST-90-92)*

**Toward Formal Development of Programs from Algebraic Specifications: Model-Theoretic Foundations**

D. Sannella and A Tarlecki

*LFCS report ECS-LFCS-92-204*

**Tail Recursion through Universal Invariants**

C B Jay

*LFCS report ECS-LFCS-92-205*

**A Set-theoretic Setting for Structuring Theories in Proof Development**

Z. Luo and R. Burstall

*LFCS report ECS-LFCS-92-206*

**A Framework for Binding Operators**

Sun Yong

*LFCS report ECS-LFCS-92-207 (also published as CST-91-92)*

**An introduction to fibrations, topos theory, the effective topos and modest sets**

Wesley Phoa

*LFCS report ECS-LFCS-92-208*

**Inductive Data Types: Well-ordering Types Revisited**

H. Goguen and Zhaohui Luo

*LFCS report ECS-LFCS-92-209*

**Listing Graphs that Satisfy First Order Sentences**

L A Goldberg

*LFCS report ECS-LFCS-92-210*

**LEGO Proof Development System: User's Manual**

Zhaohui Luo and R Pollack

*LFCS report ECS-LFCS-92-211*

**On Resolution in Fragments of Classical Linear Logic (Extended Abstract)**

J Harland and D J Pym

*LFCS report ECS-LFCS-92-212*

**A proposed categorical semantics for Pure ML**

Wesley Phoa and Michael Fourman

*LFCS report ECS-LFCS-92-213*

**From term models to domains**

Wesley Phoa

*LFCS report ECS-LFCS-92-214*

**Building domains from graph models**

Wesley Phoa

*LFCS report ECS-LFCS-92-215*

**Process-Algebraic Interpretations of Positive Linear and Relevant Logics**

Mads Dam

*LFCS report ECS-LFCS-92-216*

**CTL* and ECTL* as fragments of the modal mu-calculus**

Mads Dam

*LFCS report ECS-LFCS-92-217*

**Bisimulation Equivalence is Decidable for all Context-Free Processes**

Soren Christensen, Hans Hüttel, Colin Stirling

*LFCS report ECS-LFCS-92-218*

**Unlimp - Uniqueness as a Leitmotiv for Implementation**

Stefan Kahrs

*LFCS report ECS-LFCS-92-219*

**Verification in ASL and related specification languages**

Jorge Farrés-Casals

*LFCS report ECS-LFCS-92-220 (also published as CST-92-92)*

**Modal and Temporal Logics for Processes**

Colin Stirling

*LFCS report ECS-LFCS-92-221*

**Toward formal development of programs from algebraic specifications: parameterisation revisited**

Donald Sannella, Stefan Sokolowski and Andrzej Tarlecki

*LFCS report ECS-LFCS-92-222*

**Relational Parametricity and Local Variables**

P W O'Hearn and R D Tennent

*LFCS report ECS-LFCS-92-223*

**Fixpoints of Büchi automata**

Mads Dam

*LFCS report ECS-LFCS-92-224*

**Object-Oriented Programming Without Recursive Types**

Benjamin C Pierce and David N Turner

*LFCS report ECS-LFCS-92-225*

**An Abstract View of Objects and Subtyping**

Martin Hofmann and Benjamin C Pierce

*LFCS report ECS-LFCS-92-226*

**Representing Logics in Type Theory**

Philippa Gardner

*LFCS report ECS-LFCS-92-227 (also published as CST-93-92)*

**Formal Development of Functional Programs in Type Theory - A Case Study**

Martin Hofmann

*LFCS report ECS-LFCS-92-228*

**A Unification Algorithm for the lambda-Pi-Calculus**

David Pym

*LFCS report ECS-LFCS-92-229*

**Brewing Strong Normalization Proofs with LEGO**

Thorsten Altenkirch

*LFCS report ECS-LFCS-92-230*

**Operational Semantics Based Formal Symbolic Simulation**

K G W Goossens

*LFCS report ECS-LFCS-92-231*

**On the pi-Calculus and Linear Logic**

G Bellin and P J Scott

*LFCS report ECS-LFCS-92-232*

**Correctness Proofs of Compilers and Debuggers: an Overview of an Approach Based on Structural Operational Semantics**

Fabio Q B da Silva

*LFCS report ECS-LFCS-92-233*

**A Sub-logarithmic Communication Algorithm for the Completely Connected Optical Communication Parallel Computer**

Leslie Ann Goldberg and Mark Jerrum

*LFCS report ECS-LFCS-92-234*

**Functional Compilation from the Standard ML Core Language to Lambda Calculus**

Nick Rothwell

*LFCS report ECS-LFCS-92-235*

**Parsing in the SML Kit**

Nick Rothwell

*LFCS report ECS-LFCS-92-236*

**Miscellaneous Design Issues in the ML Kit**

Nick Rothwell

*LFCS report ECS-LFCS-92-237*

**Polymorphic Type Checking by Interpretation of Code**

Stefan Kahrs

*LFCS report ECS-LFCS-92-238*

**A Case Study in Safety-Critical Design**

Glenn Bruns

*LFCS report ECS-LFCS-92-239*

**Observational Equivaalence and Compiler Correctness**

Fabio Q B da Silva

*LFCS report ECS-LFCS-92-240*

**Correctness Proofs of Compilers and Debuggers: an Approach Based on Structural Operational Semantics**

Fabio Q B da Silva

*LFCS report ECS-LFCS-92-241 (also published as CST-95-92)*

**Deliverables: a categorical approach to program development in type theory**

Rod Burstall and James McKinna

*LFCS report ECS-LFCS-92-242*

**The Virtues of Eta-expansion**

C Barry Jay and Neil Ghani

*LFCS report ECS-LFCS-92-243*

**Decomposability, Decidability and Axiomatisability for Bisimulation Equivalence on Basic Parallel Processes**

S Christensen, Y Hirshfield and F Moller

*LFCS report ECS-LFCS-92-244*

**A Semantics for Static Type Inference**

Gordon Plotkin

*LFCS report ECS-LFCS-92-245*

**Logic Programming via Proof-Valued Computations**

David J Pym and Lincoln A Wallen

*LFCS report ECS-LFCS-92-246*

**Deliverables: a categorical approach to program development in type theory**

James Hugh McKinna

*LFCS report ECS-LFCS-92-247 (also published as CST-96-92)*

**A Synopsis on the Identification of Linear Logic Programming Languages**

James Harland and David Pym

*LFCS report ECS-LFCS-92-248*

**Action Structures**

Robin Milner

*LFCS report ECS-LFCS-92-249*

**An Algorithm for Constructing beta-eta-long normal forms**

Philippa Gardner

*LFCS report ECS-LFCS-92-250 (UNAVAILABLE)*

**Equivalences between Logics and their Representing Type Theories**

Philippa Gardner

*LFCS report ECS-LFCS-92-251*

**Newtonian Arbiters Cannot be Proven Correct**

Michael Mendler and Terry Stroup

*LFCS report ECS-LFCS-92-252*

**Hiding and Behaviour: An Institutional Approach**

Rod Burstall and Razvan Diaconescu

*LFCS report ECS-LFCS-92-253*