5. TPHOLs 1992: Leuven, Belgium

Luc J. M. Claesen, Michael J. C. Gordon (Eds.): Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992. IFIP Transactions A-20 North-Holland/Elsevier 1993, ISBN 0-444-89880-8

Mathematical Logic Issues

Thomas F. Melham: The HOL Logic Extended with Quantification over Type Variables. 3-17
Richard J. Boulton: A Lazy Approach to Fully-Expansive Theorem Proving. 19-38
Klaus Schneider, Ramayya Kumar, Thomas Kropf: Efficient Representation and Computation of Tableau Proofs. 39-57
Ching-Tsun Chou: A Note on Interactive Theorem Proving with Theorem Continuation Functions. 59-69
Ching-Tsun Chou: A Sequent Formulation of a Logic of Predicates in HOL. 71-80
Garrel Pottinger: A Classical Type Theory with Transfinite Types. 81-94

Induction

Holger Busch: Unification Based Induction. 97-116
Mark van der Voort: Introducing well-founded function definitions in HOL. 117-131
Richard J. Boulton: Boyer-Moore Automation for the HOL System. 133-142

General Modelling and Proofs

John Harrison: Constructing the real numbers in HOL. 145-164
Klaus Schneider, Ramayya Kumar, Thomas Kropf: Modelling Generic Hardware Structures by Abstract Datatypes. 165-175
Mark Aagaard, Miriam Leeser: A Methodology for Reusable Hardware Proofs. 177-196
Phillip J. Windley: Abstract Theories in HOL. 197-210
Michael McAllister: Machine Abstraction in Microprocessor Specification. 211-224

Formalizing and Modelling of Automata

Paul Loewenstein: A Formal Theory of Simulations Between Infinite Automata. 227-246
Nancy A. Day: A Comparison between Statecharts and State Transition Assertions. 247-262
Rachel Cardell-Oliver, Roger Hale, John Herbert: An Embedding of Timed Transition Systems in HOL. 263-278
Monica Nesi: Formalizing a Modal Logic for CSS in the HOL Theorem Prover. 279-294
Jim Alves-Foss: Modelling Non-Deterministic System in HOL. 295-304

Program Verification

Joakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas Långbacka: Mechanising some Advanced Refinement Concepts. 307-326
Paul Curzon: Deriving Correctness Properties of Compiled Code. 327-346
William L. Harrison, Myla Archer, Karl N. Levitt: A HOL Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language. 347-356

Hardware Description Language Semantics

John Van Tassel: A Formalisation of the VHDL Simulation Cycle. 359-374
Catia M. Angelo, Luc J. M. Claesen, Hugo De Man: The Formal Semantics Definition of a Multi-Rate DSP Specification Language in HOL. 375-394
Roger B. Hughes, Gerry Musgrave: Design-Flow Graph Partitioning. 395-404

Hardware Verification Methodologies

Saraswati Kalvala, Myla Archer, Karl N. Levitt: Implementation and Use of Annotations in HOL. 407-426
Jing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala: Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit. 427-447
Li-Guo Wang: Deriving a Correct Computer. 449-458
Roger B. Hughes, M. D. Francis, Simon Finn, Gerry Musgrave: Formal Tools in Tri-State Design in Busses. 459-475
Massimo Bombana, Patrizia Cavalloro, Giuseppe Zaza: Specification and Formal Synthesis of Digital Circuits. 475-484

Simulation in Higher Order Logic

Kees G. W. Goossens: Operational Semantics Based on Formal Symbolic Simulation. 487-506
Kelly M. Hall, Phillip J. Windley: Simulating Microprocessors from Formal Specifications. 507-525
Sreeranga P. Rajan: Executing HOL Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic. 527-536

Extended Uses of Higher Oredr Logic

Myla Archer, George Fink, Lie Yang: Linking Other Theorem Provers to HOL Using PM: Proof Manager. 539-548
Konrad Slind: Adding New Rules to an LCF-style Logic Implementation. 549-559
Elsa L. Gunter: Why we can't have SML-style datatype Declarations in HOL. 561-568