Abstract is missing.
- Mechanizing a pi-Calculus Equivalence in HOLOtmane Aït Mohamed. 1-16
- Non-primitive Recursive Function DefinitionsSten Agerholm. 17-31
- Experiments with ZF Set Theory in HOL and IsabelleSten Agerholm, Michael J. C. Gordon. 32-45
- Autotically Synthesized Term Denotation Predicates: A Proof AidPaul E. Black, Phillip J. Windley. 46-57
- On the Refinement of symmetric memory protocolsJean-Paul Bodeveix, Mamoun Filali. 58-74
- Combining Decision Procedures in the HOL SystemRichard J. Boulton. 75-89
- Deciding Cryptographic Protocol Adequacy with HOLStephen H. Brackin. 90-105
- A Practical Method for Reasoning about Distributed Systems in a Theorem ProverHolger Busch. 106-121
- A Theory of Finite MapsGraham Collins, Don Syme. 122-137
- Virtual TheoriesPaul Curzon. 138-153
- An Automata Theory Dedicated towards Formal Circuit SynthesisDirk Eisenbiegler, Ramayya Kumar. 154-169
- Interfacing HOL90 with a Functional Database Query LanguageElsa L. Gunter, Leonid Libkin. 170-185
- Floating Point Verification in HOLJohn Harrison. 186-199
- Inductive Definitions: Automation and ApplicationJohn Harrison. 200-213
- A Formulation of TLA in IsabelleSara Kalvala. 214-228
- Formal Verification of Serial Pipeline MultipliersJang Dae Kim, Shiu-Kai Chin. 229-244
- TkWinHOL: A Tool for Window Inference in HOLThomas Långbacka, Rimvydas Ruksenas, Joakim von Wright. 245-260
- Formal Verification of Counterflow Pipeline ArchitecturePaul Loewenstein. 261-276
- Deep Embedding VHDLRalf Reetz. 277-292
- HOLCF: Higher Order Logic of Computable FunctionsFranz Regensburger. 293-307
- A Mechanized Logic for Secure Key Escrow Protocol VerificationE. Thomas Schubert, Sarah Mocas. 308-323
- A New Interface for HOL - Ideas, Issues and ImplementationDon Syme. 324-339
- Very Efficient ConversionsMorten Welinder. 340-352
- Recording and Checking HOL ProofsWai Wong. 353-368
- Formalization of Planar GraphsMitsuharu Yamamoto, Shin-ya Nishizaki, Masami Hagiya, Yozo Toda. 369-384
- A Hierarchical Method for Reasoning about Distributed Programming LanguagesCui Zhang, Brian R. Becker, Mark Heckman, Karl N. Levitt, Ronald A. Olsson. 385-400