Theorem Proving in Higher Order Logics

1. Front Matter

   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

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.

• Coq
• Isabelle
• formal verification
• logic
• proof theory
• proving
• theorem proving
• verification

• Computing Laboratory, Oxford University,  

  Joe Hurd

• Computing Laboratory, Oxford University, UK

  Tom Melham

Policies and ethics