Skip to main content
SpringerLink
Log in
Book cover

Theorem Proving in Higher Order Logics

13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14-18, 2000 Proceedings

  • Conference proceedings
  • © 2000

Overview

Editors:
  1. Mark Aagaard

    1. Intel Corporation, Hillsboro, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. John Harrison

    1. Intel Corporation, Hillsboro, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 1869)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (33 papers)

  1. Front Matter

    Pages I-IX
    Download chapter 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
Back to top

Keywords

About this book

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.

Editors and Affiliations

  • Intel Corporation, Hillsboro, USA

    Mark Aagaard, John Harrison

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation