9. TPHOLs 1996: Turku, Finland

• Sten Agerholm:
  Translating Specifications in VDM-SL to PVS. 1-16
  
• Sten Agerholm, Ilya Beylin, Peter Dybjer:
  A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. 17-32
  
• David A. Basin, Stefan Friedrich:
  Modeling a Hardware Synthesis Methodology in Isabelle. 33-50
  
• Paul E. Black, Phillip J. Windley:
  Inference Rules for Programming Languages with Side Effects in Expressions. 51-60
  
• Stephen H. Brackin:
  Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. 61-76
  
• Holger Busch:
  Proving Liveness of Fair Transition Systems. 77-92
  
• Michael J. Butler, Thomas Långbacka:
  Program Derivation Using the Refinement Calculator. 93-108
  
• Graham Collins:
  A Proof Tool for Reasoning About Functional Programs. 109-124
  
• Solange Coupet-Grimal, Line Jakubiec:
  Coq and Hardware Verification: A Case Study. 125-139
  
• Bruno Dutertre:
  Elements of Mathematical Analysis in PVS. 141-156
  
• Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar:
  Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL. 157-172
  
• Andrew D. Gordon, Thomas F. Melham:
  Five Axioms of Alpha-Conversion. 173-190
  
• Michael J. C. Gordon:
  Set Theory, Higher Order Logic or Both? 191-201
  
• John Harrison:
  A Mizar Mode for HOL. 203-220
  
• John Harrison:
  Stålmarck's Algorithm as a HOL Derived Rule. 221-234
  
• Mark Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl N. Levitt, Ronald A. Olsson:
  Towards Applying the Composition Principle to Verify a Microkernel Operating System. 235-250
  
• Barbara Heyd, Pierre Crégut:
  A Modular Coding of UNITY in COQ. 251-266
  
• Douglas J. Howe:
  Importing Mathematics from HOL into Nuprl. 267-281
  
• Kolyang, Thomas Santen, Burkhart Wolff:
  A Structure Preserving Encoding of Z in Isabelle/HOL. 283-298
  
• Mats Larsson:
  Improving the Result of High-Level Synthesis Using Interactive Transformational Design. 299-314
  
• Linas Laibinis:
  Using Lattice Theory in Higher Order Logic. 315-330
  
• Dieter Nazareth, Tobias Nipkow:
  Formal Verification of Algorithm W: The Monomorphic Case. 331-345
  
• Cornelia Pusch:
  Verification of Compiler Correctness for the WAM. 347-361
  
• Bernhard Reus:
  Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. 365-380
  
• Konrad Slind:
  Function Definition in Higher-Order Logic. 381-397
  
• Alan Smaill, Ian Green:
  Higher-Order Annotated Terms for Proof Search. 399-413
  
• Sofiène Tahar, Paul Curzon:
  A Comparison of MDG and HOL for Hardware Verification. 415-430
  
• Vincent Zammit:
  A Mechanisation of Computability Theory in HOL. 431-446