Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings (Q1819255)

The articles of this volume will be reviewed individually. The preceding conference (11st, 1998) has been reviewed (see Zbl 0898.00030). Indexed articles: \textit{Völker, Norbert}, Disjoint sums over type classes in HOL, 5-18 [Zbl 0942.03013] \textit{Berghofer, Stefan; Wenzel, Markus}, Inductive datatypes in HOL -- lessons learned in formal-logic engineering, 19-36 [Zbl 0947.68128] \textit{Santen, Thomas}, Isomorphisms -- a link between the shallow and the deep, 37-54 [Zbl 0942.03011] \textit{Pfeifer, Holger; Rueß, Harald}, Polytypic proof construction, 55-72 [Zbl 0942.03012] \textit{Matthews, John}, Recursive function definition over coinductive types, 73-90 [Zbl 0944.03009] \textit{Capretta, Venanzio}, Universal algebra in type theory, 131-148 [Zbl 0947.08001] \textit{Zammit, Vincent}, On the implementation of an extensible declarative proof language, 185-202 [Zbl 0949.68139] \textit{Syme, Don}, Three tactic theorem proving, 203-220 [Zbl 0944.68162] \textit{Ambler, Simon J.; Crole, Roy L.}, Mechanized operational semantics via (co)induction, 221-238 [Zbl 0954.68093] \textit{Staples, Mark}, Representing WP semantics in Isabelle/ZF, 239-254 [Zbl 0944.68163] \textit{Schneider, Klaus; Hoffmann, Dirk W.}, A HOL conversion for translating linear time temporal logic to \(\omega\)-automata, 255-272 [Zbl 0943.03008] \textit{Grobauer, Bernd; Müller, Olaf}, From I/O automata to timed I/O automata. A solution to the ``Generalized Railroad Crossing'' in Isabelle/HOLCF, 273-289 [Zbl 0952.68128] \textit{Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène}, Importing MDG verification results into HOL, 293-310 [Zbl 0969.94503]