Higher order logic theorem proving and its applications. 8th International Workshop, Aspen Grove, UT, USA, September 11-14, 1995. Proceedings (Q1897004)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Aït Mohamed, Otmane}, Mechanizing a \(\pi\)-calculus equivalence in HOL, 1-16 [Zbl 1063.68600] \textit{Agerholm, Sten}, Non-primitive recursive function definitions, 17-31 [Zbl 1063.68640] \textit{Agerholm, Sten; Gordon, Mike}, Experiments with ZF set theory in HOL and Isabelle, 32-45 [Zbl 1063.68641] \textit{Black, Paul E.; Windley, Phillip J.}, Automatically synthesized term denotation predicates: a proof aid, 46-57 [Zbl 1063.68642] \textit{Bodeveix, J.-P.; Filali, M.}, On the refinement of symmetric memory protocols, 58-74 [Zbl 1063.68601] \textit{Boulton, Richard J.}, Combining decision procedures in the HOL system, 75-89 [Zbl 1063.68643] \textit{Brackin, Stephen H.}, Deciding cryptographic protocol adequacy with HOL, 90-105 [Zbl 1063.68644] \textit{Busch, Holger}, A practical method for reasoning about distributed systems in a theorem prover, 106-121 [Zbl 1063.68645] \textit{Collins, Graham; Syme, Donald}, A theory of finite maps, 122-137 [Zbl 1063.68646] \textit{Curzon, Paul}, Virtual theories, 138-153 [Zbl 1063.68649] \textit{Eisenbiegler, Dirk; Kumar, Ramayya}, An automata theory dedicated towards formal circuit synthesis, 154-169 [Zbl 1063.68651] \textit{Gunter, Elsa L.; Libkin, Leonid}, Interfacing HOL90 with a functional database query language, 170-185 [Zbl 1063.68583] \textit{Harrison, John}, Floating point verification in HOL, 186-199 [Zbl 1063.68652] \textit{Harrison, John}, Inductive definitions: automation and application, 200-213 [Zbl 1063.03501] \textit{Kalvala, Sara}, A formulation of TLA in Isabelle, 214-228 [Zbl 1063.68653] \textit{Kim, Jang Dae; Chin, Shiu-Kai}, Formal verification of serial pipeline multipliers, 229-244 [Zbl 1063.68654] \textit{Långbacka, Thomas; Rukšėnas, Rimvydas; von Wright, Joakim}, TkWinHOL: a tool for window inference in HOL, 245-260 [Zbl 1063.68655] \textit{Loewenstein, Paul N.}, Formal verification of counterflow pipeline architecture, 261-276 [Zbl 1063.68610] \textit{Reetz, Ralf}, Deep embedding VHDL, 277-292 [Zbl 1063.68509] \textit{Regensburger, Franz}, HOLCF: Higher order logic of computable functions, 293-307 [Zbl 1063.03503] \textit{Schubert, Tom; Mocas, Sarah}, A mechanized logic for secure key escrow protocol verification, 308-323 [Zbl 1063.68657] \textit{Syme, Donald}, A new interface for HOL -- ideas, issues and implementation, 324-339 [Zbl 1063.68658] \textit{Welinder, Morten}, Very efficient conversions, 340-352 [Zbl 1063.68659] \textit{Wong, Wai}, Recording and checking HOL proofs, 353-368 [Zbl 1063.68660] \textit{Yamamoto, Mitsuharu; Nishizaki, Shin-ya; Hagiya, Masami; Toda, Yozo}, Formalization of planar graphs, 369-384 [Zbl 1063.68661] \textit{Zhang, Cui; Becker, Brian R.; Heckman, Mark R.; Levitt, Karl; Olsson, Ron A.}, A hierarchical method for reasoning about distributed programming languages, 385-400 [Zbl 1063.68564]