8. TPHOLs 1995: Aspen Grove, UT, USA

E. Thomas Schubert, Phillip J. Windley, Jim Alves-Foss (Eds.): Higher Order Logic Theorem Proving and Its Applications, 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995, Proceedings. Lecture Notes in Computer Science 971 Springer 1995, ISBN 3-540-60275-5 BibTeX

@proceedings{DBLP:conf/tphol/1995,
  editor    = {E. Thomas Schubert and
               Phillip J. Windley and
               Jim Alves-Foss},
  title     = {Higher Order Logic Theorem Proving and Its Applications, 8th
               International Workshop,  Aspen Grove, UT, USA, September 11-14,
               1995, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {971},
  year      = {1995},
  isbn      = {3-540-60275-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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