13. TPHOLs 2000:
Portland, Oregon, USA
Mark Aagaard, John Harrison (Eds.):
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings.
Lecture Notes in Computer Science 1869 Springer 2000, ISBN 3-540-67863-8 
- 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 A. 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
Last update Tue May 21 18:07:50 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
