• People
• Events
• Research

LFCS reports 1992

• 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