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 
- 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
Last update Sat May 18 19:51:45 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
