13. TPHOLs 2000: Portland, Oregon, USA

• Antonia Balaa, Yves Bertot:
  Fix-Point Equations for Well-Founded Recursion in Type Theory. 1-16
  
• Bruno Barras:
  Programming and Computing in HOL. 17-37
  
• Stefan Berghofer, Tobias Nipkow:
  Proof Terms for Simply Typed Higher Order Logic. 38-52
  
• Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic:
  Routing Information Protocol in HOL/SPIN. 53-72
  
• Venanzio Capretta:
  Recursive Families of Inductive Types. 73-89
  
• Victor Carreño, César Muñoz:
  Aircraft Trajectory Modeling and Altering Algorithm Verification. 90-105
  
• Robert P. Colwell, Bob Brennan:
  Intel's Formal Verification Experience on the Willamette Development. 106-107
  
• Ewen Denney:
  A Prototype Proof Translator from HOL to Coq. 108-125
  
• Catherine Dubois:
  Proving ML Type Soundness Within Coq. 126-144
  
• Jacques D. Fleuriot:
  On the Mechanization of Real Analysis in Isabelle/HOL. 145-161
  
• Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
  Equational Reasoning via Partial Reflection. 162-178
  
• Michael J. C. Gordon:
  Reachability Programming in HOL98 Using BDDs. 179-196
  
• Hanne Gottliebsen:
  Transcendental Functions and Continuity Checking in PVS. 197-214
  
• Jim Grundy:
  Verified Optimizations for the Intel IA-64 Architecture. 215-232
  
• John Harrison:
  Formal Verification of IA-64 Division Algorithms. 233-251
  
• Jason Hickey, Aleksey Nogin:
  Fast Tactic-Based Theorem Proving. 252-267
  
• Martin Hofmann, Francis Tang:
  Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. 268-282
  
• M. Randall Holmes:
  A Strong and Mechanizable Grand Logic. 283-300
  
• Marieke Huisman, Bart Jacobs:
  Inheritance in Higher Order Logic: Modeling and Reasoning. 301-319
  
• Paul B. Jackson:
  Total-Correctness Refinement for Sequential Reactive Systems. 320-337
  
• Roope Kaivola, Mark Aagaard:
  Divider Circuit Verification with Model Checking and Theorem Proving. 338-355
  
• Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin:
  Specification and Verification of a Steam-Boiler with Signal-Coq. 356-371
  
• Linas Laibinis, Joakim von Wright:
  Functional Procedures in Higher-Order Logic. 372-387
  
• Pierre Letouzey, Laurent Théry:
  Formalizing Stålmarck's Algorithm in Coq. 388-405
  
• Christoph Lüth, Burkhart Wolff:
  TAS - A Generic Window Inference System. 406-423
  
• Stephan Merz:
  Weak Alternating Automata in Isabelle/HOL. 424-441
  
• Robin Milner:
  Graphical Theories of Interactive Systems: Can a Proof Assistant Help? 442
  
• Abdel Mokkedem, Tim Leonard:
  Formal Verification of the Alpha 21364 Network Protocol. 443-461
  
• Robert Pollack:
  Dependently Typed Records for Representing Mathematical Structure. 462-479
  
• Bernhard Reus, Tatjana Hein:
  Towards a Machine-Checked Java Specification Book. 480-497
  
• Konrad Slind:
  Another Look at Nested Recursion. 498-518
  
• Larry Wos, Branden Fitelson:
  Automating the Search for Answers to Open Questions. 519-525
  
• Larry Wos:
  Appendix: Conjectures Concerning Proof, Design, and Verification. 526-533