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