Theroem Proving in Higher Order Logics : 13th International Conference, TPHOLs 2000, Portland, OR, U. S. A., August 14-18, 2000 Proceedings

by Tphols 200 (2000 Portland, Or.); Aagaard, Mark; Harrison, J.

• ISBN13: 9783540678632
• ISBN10: 3540678638
• Format: Paperback
• Copyright: 2000-09-01
• Publisher: Springer Verlag

Summary

This book constitutes the refereed proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000, held in Portland, Oregon, USA in August 2000. The 29 revised full papers presented together with three invited contributions were carefully reviewed and selected from 55 submissions. All current aspects of HOL theorem proving, formal verification of hardware and software systems, and formal verification are covered. Among the HOL theorem provers evaluated are COQ, HOL, Isabelle, HOL/SPIN, PVS, and Isabelle/HOL.

Table of Contents

Fix-Point Equations for Well-Founded Recursion in Type Theory	1	(16)
Antonia Balaa
Yues Bertot
Programming and Computing in HOL	17	(21)
Bruno Barras
Proof Terms for Simply Typed Higher Order Logic	38	(15)
Stefan Berghofer
Tobias Nipkow
Routing Information Protocol in HOL/SPIN	53	(20)
Karthikeyan Bhargavan
Carl A. Gunter
Davor Obradovic
Recursive Families of Inductive Types	73	(17)
Venanzio Capretta
Aircraft Trajectory Modeling and Alerting Algorithm Verification	90	(16)
Victor Carreno
Cesar Munoz
Intel's Formal Verification Experience on the Willamette Development (Invited Talk)	106	(2)
Bob Colwell
Bob Brennan
A Prototype Proof Translator from HOL to Coq	108	(18)
Ewen Denney
Proving ML Type Soundless Within Coq	126	(19)
Catherine Dubois
On the Mechanization of Real Analysis in Isabelle/HOL	145	(17)
Jacques D. Fleuriot
Equational Reasoning via Partial Reflection	162	(17)
H. Geuvers
F. Wiedijk
J. Zwanenburg
Reachability Programming in HOL98 Using BDDs	179	(18)
Michael J. C. Gordon
Transcendental Functions and Continuity Checking in PVS	197	(18)
Hanne Gottliebsen
Verified Optimizations for the Intel IA-64 Architecture	215	(18)
Jim Grundy
Formal Verification of IA-64 Division Algorithms	233	(19)
John Harrison
Fast Tactic-Based Theorem Proving	252	(16)
Jason Hickey
Aleksey Nogin
Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover	268	(15)
Martin Hofmann
Francis Tang
A Strong and Mechanizable Grand Logic	283	(18)
M. Randall Holmes
Inheritance in Higher Order Logic: Modeling and Reasoning	301	(19)
Marieke Huisman
Bart Jacobs
Total-Correctness Refinement for Sequential Reactive Systems	320	(18)
Paul B. Jackson
Divider Circuit Verification with Model Checking and Theorem Proving	338	(18)
Roope Kaivola
Mark D. Aagaard
Specification and Verification of a Steam-Boiler with Signal-Coq	356	(16)
Mickael Kerboeuf
David Nowak
Jean-Pierre Talpin
Functional Procedures in Higher-Order Logic	372	(16)
Linas Laibinis
Joakim von Wright
Formalizing Stalmarck's Algorithm in Coq	388	(18)
Pierre Letouzey
Laurent Thery
TAS --- A Generic Window Inference System	406	(18)
Christoph Luth
Burkhart Wolff
Weak Alternating Automata in Isabelle/HOL	424	(18)
Stephan Merz
Graphical Theories of Interactive Systems: Can a Proof Assistant Help? (Invited Talk)	442	(1)
Robin Milner
Formal Verification of the Alpha 21364 Network Protocol	443	(19)
Abdel Mokkedem
Tim Leonard
Dependently Typed Records for Representing Mathematical Structure	462	(18)
Robert Pollack
Towards a Machine-Checked Java Specification Book	480	(18)
Bernhard Reus
Tatjana Hein
Another Look at Nested Recursion	498	(21)
Konrad Slind
Automating the Search for Answers to Open Questions (Invited Talk)	519	(7)
Larry Wos
Branden Fitelson
Appendix: Conjectures Concerning Proof, Design, and Verification	526	(9)
Larry Wos
Author Index	535