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