7. TPHOLs 1994: Valletta, Malta

• Sten Agerholm:
  LCF Examples in HOL. 1-16
  
• Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson:
  A Graphical Tool for Proving Unity Progress. 17-32
  
• Catia M. Angelo, Luc J. M. Claesen, Hugo De Man:
  Reasoning About a Class of Linear Systems of Equations in HOL. 33-48
  
• Jean-Paul Bodeveix, Mamoun Filali, P. Roche:
  Towards a HOL Theory and Memory. 49-64
  
• Stephen H. Brackin:
  Providing Tractable Security Analysis in HOL. 65-80
  
• N. G. de Bruijn:
  Highlighting the Lambda-free Fragment of Automath. 81-96
  
• Holger Busch:
  First-Order Automation for Higher-Order-Logic Theorem Proving. 97-112
  
• Juanito Camilleri, Vincent Zammit:
  Symbolic Animation as a Proof Tool. 113-127
  
• Nick Chapman, Simon Finn, Michael P. Fourman:
  Datatypes in L2. 128-143
  
• Ching-Tsun Chou:
  A Formal Theory of Undirected Graphs in Higher-Order Logic. 144-157
  
• Ching-Tsun Chou:
  Mechanical Verification of Distributed Algorithms in Higher-Order Logic. 158-176
  
• Paul Curzon:
  Tracking Design Changes with Formal Verification. 177-192
  
• Thomas Forster:
  Weak Systems of Set Theory Related to HOL. 193-204
  
• David A. Fura, Arun K. Somani:
  Interval-Semantic Component Models and the Efficient Verification of Transaction-Level Circiut Behavior. 205-220
  
• Brian T. Graham:
  An Interpretation of NODEN in HOL. 221-234
  
• Keith Hanna:
  Reasoning about Real Circuits. 235-253
  
• John Harrison:
  Binary Decision Diagrams as a HOL Derived Rule. 254-268
  
• Peter V. Homeier, David F. Martin:
  Trustworthy Tools for Trustworthy Programs: A Verified Verification Condition Generator. 269-284
  
• Jeffrey J. Joyce, Nancy A. Day, Michael R. Donat:
  S: A Machine Readable Specification Notation based on Higher Order Logic. 285-299
  
• Mats Larsson:
  An Engineering Approach to Formal Digital System Design. 300-315
  
• Juin-Yeu Lu, Shiu-Kai Chin:
  Generating Designs Using an Algorithmic Register Transfer Language with Formal Semantics. 316-331
  
• Thomas Långbacka:
  A HOL Formalisation of the Temporal Logic of Actions. 332-345
  
• Savi Maharaj, Elsa L. Gunter:
  Studying the ML Module System in Hol. 346-361
  
• I. S. W. B. Prasetya:
  Towards a Mechanically Supported and Compositional Calculus to Design Destributed Algorithms. 362-377
  
• Ralf Reetz, Thomas Kropf:
  Simplifying Deep Embedding: A Formalised Code Generator. 378-390
  
• Klaus Schneider, Ramayya Kumar, Thomas Kropf:
  Automating Verification by Functional Abstraction at the System Level. 391-406
  
• Konrad Slind:
  A Parameterized Proof Manager. 407-423
  
• Sofiène Tahar, Ramayya Kumar:
  Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL. 424-439
  
• Phillip J. Windley:
  Specifying Instruction-Set Architectures in HOL: A Primer. 440-455
  
• Joakim von Wright:
  Representing Higher-Order Logic Proofs in HOL. 456-470