Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings (Q1578436)

The articles of mathematical interest will be reviewed individually. The preceding conference (12th, 1999) has been reviewed (see Zbl 0929.00038). Indexed articles: \textit{Balaa, Antonia; Bertot, Yves}, Fix-point equations for well-founded recursion in type theory, 1-16 [Zbl 0974.68183] \textit{Barras, Bruno}, Programming and computing in HOL, 17-37 [Zbl 0974.68187] \textit{Berghofer, Stefan; Nipkow, Tobias}, Proof terms for simply typed higher order logic, 38-52 [Zbl 0974.03013] \textit{Bhargavan, Karthikeyan; Gunter, Carl A.; Obradovic, Davor}, Routing information protocol in HOL/SPIN, 53-72 [Zbl 0974.68010] \textit{Capretta, Venanzio}, Recursive families of inductive types, 73-89 [Zbl 0974.03014] \textit{Carreño, Víctor; Muñoz, César}, Aircraft trajectory modeling and alerting algorithm verification, 90-105 [Zbl 0974.68548] \textit{Colwell, Bob; Brennan, Bob}, Intel's formal verification experience on the Willamette development, 106-107 [Zbl 0974.68558] \textit{Denney, Ewen}, A prototype proof translator from HOL to Coq, 108-125 [Zbl 0974.68533] \textit{Dubois, Catherine}, Proving ML type soundness within Coq, 126-144 [Zbl 0974.68188] \textit{Fleuriot, Jacques D.}, On the mechanization of real analysis in Isabelle/HOL, 145-161 [Zbl 0974.68186] \textit{Geuvers, H.; Wiedijk, F.; Zwanenburg, J.}, Equational reasoning via partial reflection, 162-178 [Zbl 0974.68182] \textit{Gordon, Michael J. C.}, Reachability programming in HOL98 using BDDs, 179-196 [Zbl 0974.68189] \textit{Gottliebsen, Hanne}, Transcendental functions and continuity checking in PVS, 197-214 [Zbl 0974.68190] \textit{Grundy, Jim}, Verified optimization for the Intel IA-64 architecture, 215-232 [Zbl 0974.68567] \textit{Harrison, John}, Formal verification of IA-64 division algorithms, 233-251 [Zbl 0974.68535] \textit{Hickey, Jason; Nogin, Aleksey}, Fast tactic-based theorem proving, 252-267 [Zbl 0974.68534] \textit{Hofmann, Martin; Tang, Francis}, Implementing a program logic of objects in a higher-order logic theorem prover, 268-282 [Zbl 0974.68185] \textit{Holmes, M. Randall}, A strong and mechanizable grand logic, 283-300 [Zbl 0974.03012] \textit{Huisman, Marieke; Jacobs, Bart}, Inheritance in higher order logic: Modeling and reasoning, 301-319 [Zbl 0974.68033] \textit{Jackson, Paul B.}, Total-correctness refinement for sequential reactive systems, 320-337 [Zbl 0974.68119] \textit{Kaivola, Roope; Aagaard, Mark D.}, Divider circuit verification with model checking and theorem proving, 338-355 [Zbl 0974.68519] \textit{Kerbœuf, Mickaël; Nowak, David; Talpin, Jean-Pierre}, Specification and verification of a steam-boiler with Signal-Coq, 356-371 [Zbl 0974.68522] \textit{Laibinis, Linas; von Wright, Joakim}, Functional procedures in higher-order logic, 372-387 [Zbl 0974.68506] \textit{Letouzey, Pierre; Théry, Laurent}, Formalizing Stålmarck's algorithm in Coq, 388-405 [Zbl 0974.68184] \textit{Lüth, Christoph; Wolff, Burkhart}, TAS -- a generic window inference system, 406-423 [Zbl 0974.68507] \textit{Merz, Stephan}, Weak alternating automata in Isabelle/HOL, 424-441 [Zbl 0974.68090] \textit{Milner, Robin}, Graphical theories of interactive systems: Can a proof assistant help?, 442 [Zbl 0974.68555] \textit{Mokkedem, Abdel; Leonard, Tim}, Formal verification of the Alpha 21364 network protocol, 443-461 [Zbl 0974.68553] \textit{Pollack, Robert}, Dependently typed records for representing mathematical structure, 462-479 [Zbl 0974.68181] \textit{Reus, Bernhard; Hein, Tatjana}, Towards a machine-checked Java specification book, 480-497 [Zbl 0974.68505] \textit{Slind, Konrad}, Another look at nested recursion, 498-518 [Zbl 0974.68180] \textit{Wos, Larry; Fitelson, Branden}, Automating the search for answers to open questions, 519-525 [Zbl 0974.68538] \textit{Wos, Larry}, Appendix: conjectures concerning proof, design, and verification, 526-533 [Zbl 0974.68537]