Theorem Proving in Higher Order Logics

1. Front Matter

   Pages I-IX

   PDF

2. Fix-Point Equations for Well-Founded Recursion in Type Theory

   • Antonia Balaa, Yves Bertot

   Pages 1-16

3. Programming and Computing in HOL

   • Bruno Barras

   Pages 17-37

4. Proof Terms for Simply Typed Higher Order Logic

   • Stefan Berghofer, Tobias Nipkow

   Pages 38-52

5. Routing Information Protocol in HOL/SPIN

   • Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic

   Pages 53-72

6. Recursive Families of Inductive Types

   • Venanzio Capretta

   Pages 73-89

7. Aircraft Trajectory Modeling and Alerting Algorithm Verification

   • Victor Carreño, César Muñoz

   Pages 90-105

8. Intel’s Formal Verification Experience on the Willamette Development

   • Bob Colwell, Bob Brennan

   Pages 106-107

9. A Prototype Proof Translator from HOL to Coq

   • Ewen Denney

   Pages 108-125

10. Proving ML Type Soundness Within Coq

    • Catherine Dubois

    Pages 126-144

11. On the Mechanization of Real Analysis in Isabelle/HOL

    • Jacques D. Fleuriot

    Pages 145-161

12. Equational Reasoning via Partial Reflection

    • H. Geuvers, F. Wiedijk, J. Zwanenburg

    Pages 162-178

13. Reachability Programming in HOL98 Using BDDs

    • Michael J. C. Gordon

    Pages 179-196

14. Transcendental Functions and Continuity Checking in PVS

    • Hanne Gottliebsen

    Pages 197-214

15. Verified Optimizations for the Intel IA-64 Architecture

    • Jim Grundy

    Pages 215-232

16. Formal Verification of IA-64 Division Algorithms

    • John Harrison

    Pages 233-251

17. Fast Tactic-Based Theorem Proving

    • Jason Hickey, Aleksey Nogin

    Pages 252-267

18. Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover

    • Martin Hofmann, Francis Tang

    Pages 268-282

19. A Strong and Mechanizable Grand Logic

    • M. Randall Holmes

    Pages 283-300

20. Inheritance in Higher Order Logic: Modeling and Reasoning

    • Marieke Huisman, Bart Jacobs

    Pages 301-319

This volume is the proceedings of the 13th International Conference on Theo­ rem Proving in Higher Order Logics (TPHOLs 2000) held 14-18 August 2000 in Portland, Oregon, USA. Each of the 55 papers submitted in the full rese­ arch category was refereed by at least three reviewers who were selected by the program committee. Because of the limited space available in the program and proceedings, only 29 papers were accepted for presentation and publication in this volume. In keeping with tradition, TPHOLs 2000 also offered a venue for the presen­ tation of work in progress, where researchers invite discussion by means of a brief preliminary talk and then discuss their work at a poster session. A supplemen­ tary proceedings containing associated papers for work in progress was published by the Oregon Graduate Institute (OGI) as technical report CSE-00-009. The organizers are grateful to Bob Colwell, Robin Milner and Larry Wos for agreeing to give invited talks. Bob Colwell was the lead architect on the Intel P6 microarchitecture, which introduced a number of innovative techniques and achieved enormous commercial success. As such, he is ideally placed to offer an industrial perspective on the challenges for formal verification. Robin Milner contributed many key ideas to computer theorem proving, and to functional programming, through his leadership of the influential Edinburgh LCF project.

• Automated Deduction
• Formal Methods
• Hardware Verification
• Higher Order Logic
• Isabelle
• Logic Design
• Mathematical Logic
• Model Checking
• SPIN
• formal verification
• proving
• theorem proving
• verification

• Intel Corporation, Hillsboro, USA

  Mark Aagaard, John Harrison

Policies and ethics