ESOP '92

Model checking and boolean graphs.- SIGNAL as a model for real-time and hybrid systems.- Towards an adequate notion of observation.- Proving safety of speculative load instructions at compile-time.- Typed norms.- Compositional refinements in multiple blackboard systems.- Fully persistent arrays for efficient incremental updates and voluminous reads.- Back to direct style.- Extraction of strong typing laws from action semantics definitions.- Detecting determinate computations by bottom-up abstract interpretation.- ELIOS-OBJ theorem proving in a specification language.- Incremental garbage collection without tags.- Approximate fixed points in abstract interpretation.- Dynamic typing.- Automatic parallelization of lazy functional programs.- Reversing abstract interpretations.- A theory of qualified types.- A semantics for multiprocessor systems.- Interprocedural type propagation for object-oriented languages.- Using the Centaur system for data-parallel SIMD programming: a case study.- The tensor product in Wadler's analysis of lists.- Basic superposition is complete.- Observers for linear types.- Type inference for partial types is decidable.- A provably correct compiler generator.- An adequate operational semantics of sharing in lazy evaluation.- Modules for a model-oriented specification language: A proposal for metasoft.- Typing references by effect inference.