Higher Order Logic Theorem Proving and its Applications

Preface. Conference Organization. Mathematical Logic Issues. The HOL Logic Extended with Quantification over Type Variables (T.F. Melham). A Lazy Approach to Fully-Expansive Theorem Proving (R.J. Boulton). Efficient Representation and Computation of Tableaux Proofs (K. Schneider, R. Kumar, T. Kropf). A Note on Interactive Theorem Proving with Theorem Continuation Functions (C.-T. Chou). A Sequent Formulation of a Logic of Predicates in HOL (C.-T. Chou). A Classical Type Theory with Transfinite Types (G. Pottinger). Induction. Unification-Based Induction (H. Busch). Introducing Well-Founded Function Definitions in HOL (M. van der Voort). Boyer-Moore Automation for the HOL System (R.J. Boulton). General Modelling and Proofs. Constructing the Real Numbers in HOL (J. Harrison). Modelling Generic Hardware Structures by Abstract Datatypes (K. Schneider, R. Kumar, T. Kropf). A Methodology for Reusable Hardware Proofs (M. Aagaard, M. Leeser). Abstract Theories in HOL (P.J. Windley). Machine Abstraction in Microprocessor Specification (M. McAllister). Formalizing and Modelling of Automata. A Formal Theory of Simulations Between Infinite Automata (P. Loewenstein). A Comparison between Statecharts and State Transition Assertions (N. Day). An Embedding of Timed Transition Systems in HOL (R. Cardell-Oliver, R. Hale, J. Herbert). Formalizing a Modal Logic for CSS in the HOL Theorem Prover (M. Nesi). Modelling Non-Deterministic Systems in HOL (J. Alves-Foss). Program Verification. Mechanising Some Advanced Refinement Concepts (J. von Wright, J. Hekanaho, P. Luostarinen, T. Langbåcka). Deriving Correctness Properties of Compiled Code (P. Curzon). A HOL Mechanization of the Axiomatic Semantics of a Simple Distributed Programming Language (W.L. Harrison, M. Archer, K.N. Levitt). Hardware Description Language Semantics. A Formalisation of the VHDL Simulation Cycle (J.P. Van Tassel). The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL (C. Angelo, L. Claesen, H. De Man). Design-Flow Graph Partitioning (R.B. Hughes, G. Musgrave). Hardware Verification Methodologies. Implementation and use of Annotations in HOL (S. Kalvala, M. Archer, K.N. Levitt). Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit (J. Pan, K.N. Levitt, M. Archer, S. Kalvala). Deriving a Correct Computer (L.-G. Wang). Formal Tools for Tri-State Design in Busses (R.B. Hughes, M.D. Francis, S.P. Finn, G. Musgrave). Specification and Formal Synthesis of Digital Circuits (M. Bombana, P. Cavalloro, G. Zaza). Simulation in Higher Order Logic. Operational Semantics Based Formal Symbolic Simulation (K.G.W. Goosens). Simulating Microprocessors from Formal Specifications (K.M. Hall, P.J. Windley). Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic (P.S. Rajan). Extended Uses of Higher Order Logic. Linking Other Theorem Provers to HOL Using PM: Proof Manager (M. Archer, G. Fink, L. Yang). Adding New Rules to an LCF-Style Logic Implementation (K. Slind). Why We Can't Have SML Style Declarations in HOL (E.L. Gunter).