Abstract is missing.
- The HOL Logic Extended with Quantification over Type VariablesThomas F. Melham. 3-17
- A Lazy Approach to Fully-Expansive Theorem ProvingRichard J. Boulton. 19-38
- Efficient Representation and Computation of Tableau ProofsKlaus Schneider, Ramayya Kumar, Thomas Kropf. 39-57
- A Note on Interactive Theorem Proving with Theorem Continuation FunctionsChing-Tsun Chou. 59-69
- A Sequent Formulation of a Logic of Predicates in HOLChing-Tsun Chou. 71-80
- A Classical Type Theory with Transfinite TypesGarrel Pottinger. 81-94
- Unification Based InductionHolger Busch. 97-116
- Introducing well-founded function definitions in HOLMark van der Voort. 117-131
- Boyer-Moore Automation for the HOL SystemRichard J. Boulton. 133-142
- Constructing the real numbers in HOLJohn Harrison. 145-164
- Modelling Generic Hardware Structures by Abstract DatatypesKlaus Schneider, Ramayya Kumar, Thomas Kropf. 165-175
- A Methodology for Reusable Hardware ProofsMark Aagaard, Miriam Leeser. 177-196
- Abstract Theories in HOLPhillip J. Windley. 197-210
- Machine Abstraction in Microprocessor SpecificationMichael McAllister. 211-224
- A Formal Theory of Simulations Between Infinite AutomataPaul Loewenstein. 227-246
- A Comparison between Statecharts and State Transition AssertionsNancy A. Day. 247-262
- An Embedding of Timed Transition Systems in HOLRachel Cardell-Oliver, Roger Hale, John Herbert. 263-278
- Formalizing a Modal Logic for CSS in the HOL Theorem ProverMonica Nesi. 279-294
- Modelling Non-Deterministic System in HOLJim Alves-Foss. 295-304
- Mechanising some Advanced Refinement ConceptsJoakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas LĂ„ngbacka. 307-326
- Deriving Correctness Properties of Compiled CodePaul Curzon. 327-346
- A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming LanguageWilliam L. Harrison, Myla Archer, Karl N. Levitt. 347-356
- A Formalisation of the VHDL Simulation CycleJohn Van Tassel. 359-374
- The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOLCatia M. Angelo, Luc J. M. Claesen, Hugo De Man. 375-394
- Design-Flow Graph PartitioningRoger B. Hughes, Gerry Musgrave. 395-404
- Implementation and Use of Annotations in HOLSaraswati Kalvala, Myla Archer, Karl N. Levitt. 407-426
- Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing UnitJing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala. 427-447
- Deriving a Correct ComputerLi-Guo Wang. 449-458
- Formal Tools in Tri-State Design in BussesRoger B. Hughes, M. D. Francis, Simon Finn, Gerry Musgrave. 459-475
- Specification and Formal Synthesis of Digital CircuitsMassimo Bombana, Patrizia Cavalloro, Giuseppe Zaza. 475-484
- Operational Semantics Based on Formal Symbolic SimulationKees G. W. Goossens. 487-506
- Simulating Microprocessors from Formal SpecificationsKelly M. Hall, Phillip J. Windley. 507-525
- Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order LogicSreeranga P. Rajan. 527-536
- Linking Other Theorem Provers to HOL Using PM: Proof ManagerMyla Archer, George Fink, Lie Yang. 539-548
- Adding New Rules to an LCF-style Logic ImplementationKonrad Slind. 549-559
- Why we can t have SML-style datatype Declarations in HOLElsa L. Gunter. 561-568