Skip to main content
SpringerLink
Log in

Theorem Proving in Higher Order Logics

18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings

  • Conference proceedings
  • © 2005

Overview

Editors:
  1. Joe Hurd

    1. Computing Laboratory, Oxford University,  

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Tom Melham

    1. Computing Laboratory, Oxford University, UK

    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 3603)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Included in the following conference series:

Conference proceedings info: TPHOLs 2005.

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 (26 papers)

  1. Front Matter

    Download chapter PDF

  2. Invited Papers

    1. On the Correctness of Operating System Kernels

      • Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, Wolfgang Paul
      Pages 1-16

    2. Alpha-Structural Recursion and Induction

      • Andrew M. Pitts
      Pages 17-34

  3. Regular Papers

    1. Shallow Lazy Proofs

      • Hasan Amjad
      Pages 35-49

    2. Mechanized Metatheory for the Masses: The PoplMark Challenge

      • Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell et al.
      Pages 50-65

    3. A Structured Set of Higher-Order Problems

      • Christoph E. Benzmüller, Chad E. Brown
      Pages 66-81

    4. Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS

      • Néstor Cataño
      Pages 82-97

    5. Proving Equalities in a Commutative Ring Done Right in Coq

      • Benjamin Grégoire, Assia Mahboubi
      Pages 98-113

    6. A HOL Theory of Euclidean Space

      • John Harrison
      Pages 114-129

    7. A Design Structure for Higher Order Quotients

      • Peter V. Homeier
      Pages 130-146

    8. Axiomatic Constructor Classes in Isabelle/HOLCF

      • Brian Huffman, John Matthews, Peter White
      Pages 147-162

    9. Meta Reasoning in ACL2

      • Warren A. Hunt Jr, Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
      Pages 163-178

    10. Reasoning About Java Programs with Aliasing and Frame Conditions

      • Claude Marché, Christine Paulin-Mohring
      Pages 179-194

    11. Real Number Calculations and Theorem Proving

      • César Muñoz, David Lester
      Pages 195-210

    12. Verifying a Secure Information Flow Analyzer

      • David A. Naumann
      Pages 211-226

    13. Proving Bounds for Real Linear Programs in Isabelle/HOL

      • Steven Obua
      Pages 227-244

    14. Essential Incompleteness of Arithmetic Verified by Coq

      • Russell O’Connor
      Pages 245-260

    15. Verification of BDD Normalization

      • Veronika Ortner, Norbert Schirmer
      Pages 261-277

    16. Extensionality in the Calculus of Constructions

      • Nicolas Oury
      Pages 278-293

    17. A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic

      • Tom Ridge, James Margetson
      Pages 294-309
Back to top

Other volumes

  1. Theorem Proving in Higher Order Logics

Keywords

About this book

This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22–25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005.

Editors and Affiliations

  • Computing Laboratory, Oxford University,  

    Joe Hurd

  • Computing Laboratory, Oxford University, UK

    Tom Melham

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation