4. TPHOLs 1991: Davis, CA, USA

Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (Eds.): Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA. IEEE Computer Society 1992

Tutorial Papers

Michael J. C. Gordon: Introduction to the HOL System. 2-3
Sara Kalvala: HOL Around the World. 4-12
John Herbert: Dealing With Temporal Complexity in Hardware Verification. 13-21
Shiu-Kai Chin: Verifying Arithmetic Hardware in Higher-Order Logic. 22-31
Phillip J. Windley: The Practical Verification of Microprocessor Designs. 32-37
E. Thomas Schubert: Verification of Integrated Subsystems. 38-51
Roger Hale: Reasoning About Software. 52-58
Rachel Cardell-Oliver: On the use of the HOL system for Protocol Verification. 59-62
William L. Harrison, Karl N. Levitt: Mechanizing Security in HOL. 63-66
Paul Loewenstein: Learning to use HOL. 67-74

Workshop Papers

Kurt Keutzer: The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me Lately. 77-86
E. Thomas Schubert: Verification of Composed Hardware Systems Using CCS. 88-95
J. W. Gambles, Phillip J. Windley: An HOL Theory for Logic States with Indeterminate Strengths. 96-103
X. Wang, Edward P. Stabler: Formalization of VHDL Synthesis Procedure in Higher-Order Logic. 106-120
Shiu-Kai Chin, Graham M. Birtwistle: Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic. 121-129
Simon Bainbridge, Albert John Camilleri, Roger Fleming: Industrial Application of Theorem Proving to System Level Design. 130-142
Richard Gerber, Elsa L. Gunter, Insup Lee: Implementing a Real-Time Process Algebra in HOL. 144-154
Joakim von Wright: Mechanising the Temporal Logic of Actions in HOL. 155-159
D. Shepherd: Using HOL to produce custom verification tools. 162-169
Ramayya Kumar, Thomas Kropf, Klaus Schneider: Integrating a First-Order Automatic Prover in the HOL Environment. 170-176
Jim Grundy: Window Inference in the HOL System. 177-189
Ramayya Kumar, Thomas Kropf, Klaus Schneider: First Steps Towards Automating Hardware Proofs in HOL. 190-193
John M. Rushby: Design Choices in Specification Languages and Verification Systems. 195-204
Sten Agerholm: Mechanizing Program Verification in HOL. 208-222
Rachel E. O. Roxas, Malcolm C. Newey: Proof of Program Transformations. 223-230
Joakim von Wright, Kaisa Sere: Program Transformations and Refinements in HOL. 231-239
David F. Martin, R. J. Toal: Case Studies in Compiler Correctness Using HOL. 242-252
Paul Curzon: A Verified Compiler for a Structured Assembly Language. 253-262 Jim Alves-Foss, Karl N. Levitt: Mechanical Verification of Secure Distributed Systems in Higher Order Logic. 263-278
R. D. Arthan: A Report on ICL HOL. 280-283
George Fink, Myla Archer, Lie Yang: PM: A Proof Manager for HOL and Other Provers. 286-304
Sara Kalvala: Developing an Interface for HOL. 305-317
Matt Kaufmann: An Informal Discussion of Issues in Mechanically-Assisted Reasoning. 318-337
Catia M. Angelo, Diederik Verkest, Luc J. M. Claesen, Hugo De Man: Formal Hardware Verification in HOL and in Boyer-Moore: A Comparative Analysis. 340-347
Thomas F. Melham: A Package for Inductive Relation Definitions in HOL. 350-357
W. Ploegaerts, Luc J. M. Claesen, Hugo De Man: Defining Recursive Functions in HOL. 358-366
Flemming Andersen, Kim Dam Petersen: Recursive Boolean Functions in HOL. 367-377
Malcolm C. Newey: Proof Based Computation. 380-383
E. de Barros Lucena: Reasoning about Petri Nets in HOL. 384-394
W. Wong: A Simple Graph Theory and Its Application in Railway Signalling. 395-409