6. HUG 1993: Vancouver, BC, Canada

• Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson:
  Program Verification using HOL-UNITY. 1-15
  
• Kim Dam Petersen:
  Graph model of LAMBDA in Higher Order Logic. 16-28
  
• Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark Heckman, Gregory D. Benson:
  Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL. 29-42
  
• Don Syme:
  Reasoning with the Formal Definition of Standard ML in HOL. 43-60
  
• Myra Van Inwegen, Elsa L. Gunter:
  HOL-ML. 61-74
  
• Kees G. W. Goossens:
  Stucture and Behaviour in Hardware Verification. 75-88
  
• Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
  Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL. 89-100
  
• Dirk Eisenbiegler, Klaus Schneider, Ramayya Kumar:
  A Functional Approach for Formalizing Regular Hardware Structures. 101-114
  
• Laurent Théry:
  A Proof Development System for HOL. 115-128
  
• Rachel E. O. Roxas:
  A HOL Package for Reasoning about Relations Defined by Mutual Induction. 129-140
  
• Elsa L. Gunter:
  A Broader Class of Trees for Recursive Type Definitions for HOL. 141-154
  
• David Lorge Parnas:
  Some Theorems We Should Prove. 155-162
  
• John M. Rushby, Mandayam K. Srivas:
  Using PVS to Prove Some Theorems Of David Parnas. 163-173
  
• John Harrison, Laurent Théry:
  Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. 174-184
  
• Jeffrey J. Joyce, Carl-Johan H. Seger:
  The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. 185-198
  
• Juin-Yeu Lu, Shiu-Kai Chin:
  Linking HOL to a VLSI CAD System. 199-212
  
• Klaus Schneider, Ramayya Kumar, Thomas Kropf:
  Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic. 213-226
  
• Anthony McIsaac:
  A Formalization of Abstraction in LAMBDA. 227-238
  
• Tej Arora, Tony Leung, Karl N. Levitt, E. Thomas Schubert, Phillip J. Windley:
  Report on the UCD Microcoded Viper Verification Project. 239-252
  
• Zheng Zhu, Jeffrey J. Joyce, Carl-Johan H. Seger:
  Verification of the Tamarack-3 Microprocessor in a Hybrid Verification Environment. 253-266
  
• David A. Fura, Phillip J. Windley, Arun K. Somani:
  Abstraction Techniques for Modeling Real-World Interface Chips. 267-280
  
• Sofiène Tahar, Ramayya Kumar:
  Implementing a Methodology for Formally Verifying RISC Processors in HOL. 281-294
  
• Sten Agerholm:
  Domain Theory in HOL. 295-309
  
• Ching-Tsun Chou:
  Predicates, Temporal Logic, and Simulations. 310-323
  
• I. S. W. B. Prasetya:
  Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties. 324-337
  
• Nancy A. Day, Jeffrey J. Joyce:
  The Semantics of Statecharts in HOL. 338-351
  
• Monica Nesi:
  Value-Passing CCS in HOL. 352-365
  
• Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi:
  TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. 366-370
  
• Wai Wong:
  Modelling Bit Vectors in HOL: the word library. 371-384
  
• Klaus Schneider, Ramayya Kumar, Thomas Kropf:
  Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification. 385-398
  
• Mark Aagaard, Miriam Leeser, Phillip J. Windley:
  Toward a Super Duper Hardware Tactic. 399-412
  
• Andrew D. Gordon:
  A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion. 413-425
  
• John Harrison:
  A HOL Decision Procedure for Elementary Real Algebra. 426-435
  
• Konrad Slind:
  AC Unification in HOL90. 436-449
  
• Stephen H. Brackin, Shiu-Kai Chin:
  Server-Process Restrictiveness in HOL. 450-463
  
• Matthew J. Morley:
  Safety in Railway Signalling Data: A Behavioural Analysis. 464-474
  
• I. S. W. B. Prasetya:
  On the Style of Mechanical Proving. 475-488
  
• Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger:
  From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation. 489-500
  
• Victor Carreño:
  Verification in Higher Order Logic of Mutual Exclusion Algorithm. 501-513
  
• Sara Kalvala:
  Using Isabelle to Prove Simple Theorems. 514-517