zbMATH — the first resource for mathematics

Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14–18, 2000. Proceedings. (English) Zbl 0944.00036
Lecture Notes in Computer Science. 1869. Berlin: Springer. ix, 535 p. (2000).

Show indexed articles as search result.

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

00B25 Proceedings of conferences of miscellaneous specific interest
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
Coq; Isabelle/HOL
Full Text: DOI