• People
• Events
• Research

LFCS reports 1991

• 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)