Theorem Proving in Higher Order Logics

1. Front Matter

   PDF

2. Error Analysis of Digital Filters Using Theorem Proving

   • Behzad Akbarpour, Sofiène Tahar

   Pages 1-17

3. Verifying Uniqueness in a Logical Framework

   • Penny Anderson, Frank Pfenning

   Pages 18-33

4. A Program Logic for Resource Verification

   • David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano

   Pages 34-49

5. Proof Reuse with Extended Inductive Types

   • Olivier Boite

   Pages 50-65

6. Hierarchical Reflection

   • Luís Cruz-Filipe, Freek Wiedijk

   Pages 66-81

7. Correct Embedded Computing Futures

   • Al Davis

   Pages 82-82

8. Higher Order Rippling in IsaPlanner

   • Lucas Dixon, Jacques Fleuriot

   Pages 83-98

9. A Mechanical Proof of the Cook-Levin Theorem

   • Ruben Gamboa, John Cowles

   Pages 99-116

10. Formalizing the Proof of the Kepler Conjecture

    • Thomas Hales

    Pages 117-117

11. Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code

    • Nadeem Abdul Hamid, Zhong Shao

    Pages 118-135

12. Extensible Hierarchical Tactic Construction in a Logical Framework

    • Jason Hickey, Aleksey Nogin

    Pages 136-151

13. Theorem Reuse by Proof Term Transformation

    • Einar Broch Johnsen, Christoph Lüth

    Pages 152-167

14. Proving Compatibility Using Refinement

    • Michael Jones, Aaron Benson, Dan Delorey

    Pages 168-183

15. Java Program Verification via a JVM Deep Embedding in ACL2

    • Hanbing Liu, J. Strother Moore

    Pages 184-200

16. Reasoning About CBV Functional Programs in Isabelle/HOL

    • John Longley, Randy Pollack

    Pages 201-216

17. Proof Pearl: From Concrete to Functional Unparsing

    • Jean-François Monin

    Pages 217-224

18. A Decision Procedure for Geometry in Coq

    • Julien Narboux

    Pages 225-240

19. Recursive Function Definition for Types with Binders

    • Michael Norrish

    Pages 241-256

20. Abstractions for Fault-Tolerant Distributed System Verification

    • Lee Pike, Jeffrey Maddalon, Paul Miner, Alfons Geser

    Pages 257-270

This volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14–17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higher-order logics as well as related topics in theorem proving and veri?cation. There were 42 papers submitted to TPHOLs 2004 in the full research ca- gory, each of which was refereed by at least 3 reviewers selected by the program committee. Of these submissions, 21 were accepted for presentation at the c- ference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2004 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 c- taining papers about in-progress work was published as a 2004 technical report of the School of Computing at the University of Utah. The organizers are grateful to Al Davis, Thomas Hales, and Ken McMillan for agreeing to give invited talks at TPHOLs 2004. The TPHOLs conference traditionally changes continents each year in order to maximize the chances that researchers from around the world can attend.

• Automat
• Isabelle
• automated deduction
• computability
• logic
• proof theory
• proving
• theorem proving
• verification

• School of Computing, University of Utah,  

  Konrad Slind

• Electrical and Computer Engineering Department, Utah State University, Logan, USA

  Annette Bunker

• School of Computing, Univ. of Utah, Salt Lake City, USA

  Ganesh Gopalakrishnan

Policies and ethics