8. TPHOLs 1995: Aspen Grove, UT, USA

• Otmane Aït Mohamed:
  Mechanizing a pi-Calculus Equivalence in HOL. 1-16
  
• Sten Agerholm:
  Non-primitive Recursive Function Definitions. 17-31
  
• Sten Agerholm, Michael J. C. Gordon:
  Experiments with ZF Set Theory in HOL and Isabelle. 32-45
  
• Paul E. Black, Phillip J. Windley:
  Autotically Synthesized Term Denotation Predicates: A Proof Aid. 46-57
  
• Jean-Paul Bodeveix, Mamoun Filali:
  On the Refinement of symmetric memory protocols. 58-74
  
• Richard J. Boulton:
  Combining Decision Procedures in the HOL System. 75-89
  
• Stephen H. Brackin:
  Deciding Cryptographic Protocol Adequacy with HOL. 90-105
  
• Holger Busch:
  A Practical Method for Reasoning about Distributed Systems in a Theorem Prover. 106-121
  
• Graham Collins, Don Syme:
  A Theory of Finite Maps. 122-137
  
• Paul Curzon:
  Virtual Theories. 138-153
  
• Dirk Eisenbiegler, Ramayya Kumar:
  An Automata Theory Dedicated towards Formal Circuit Synthesis. 154-169
  
• Elsa L. Gunter, Leonid Libkin:
  Interfacing HOL90 with a Functional Database Query Language. 170-185
  
• John Harrison:
  Floating Point Verification in HOL. 186-199
  
• John Harrison:
  Inductive Definitions: Automation and Application. 200-213
  
• Sara Kalvala:
  A Formulation of TLA in Isabelle. 214-228
  
• Jang Dae Kim, Shiu-Kai Chin:
  Formal Verification of Serial Pipeline Multipliers. 229-244
  
• Thomas Långbacka, Rimvydas Ruksenas, Joakim von Wright:
  TkWinHOL: A Tool for Window Inference in HOL. 245-260
  
• Paul Loewenstein:
  Formal Verification of Counterflow Pipeline Architecture. 261-276
  
• Ralf Reetz:
  Deep Embedding VHDL. 277-292
  
• Franz Regensburger:
  HOLCF: Higher Order Logic of Computable Functions. 293-307
  
• E. Thomas Schubert, Sarah Mocas:
  A Mechanized Logic for Secure Key Escrow Protocol Verification. 308-323
  
• Don Syme:
  A New Interface for HOL - Ideas, Issues and Implementation. 324-339
  
• Morten Welinder:
  Very Efficient Conversions. 340-352
  
• Wai Wong:
  Recording and Checking HOL Proofs. 353-368
  
• Mitsuharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya, Yozo Toda:
  Formalization of Planar Graphs. 369-384
  
• Cui Zhang, Brian R. Becker, Mark Heckman, Karl N. Levitt, Ronald A. Olsson:
  A Hierarchical Method for Reasoning about Distributed Programming Languages. 385-400