Theorem Proving in Higher Order Logics: 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings

Front Cover
Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan
Springer Science & Business Media, Sep 1, 2004 - Computers - 340 pages
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Error Analysis of Digital Filters Using Theorem Proving
1
Verifying Uniqueness in a Logical Framework
18
A Program Logic for Resource Verification
34
Proof Reuse with Extended Inductive Types
50
Hierarchical Reflection
66
Correct Embedded Computing Futures
82
Higher Order Rippling in IsaPlanner
83
A Mechanical Proof of the CookLevin Theorem
99
Java Program Verification via a JVM Deep Embedding in ACL2
184
Reasoning About CBV Functional Programs in IsabelleHOL
201
From Concrete to Functional Unparsing
217
A Decision Procedure for Geometry in Coq
225
Recursive Function Definition for Types with Binders
241
Abstractions for FaultTolerant Distributed System Verification
257
Formalizing Integration Theory with an Application to Probabilistic Algorithms
271
Formalizing Java Dynamic Loading in HOL
287

Formalizing the Proof of the Kepler Conjecture
117
Interfacing Hoare Logic and Type Systems for Foundational ProofCarrying Code
118
Extensible Hierarchical Tactic Construction in a Logical Framework
136
Theorem Reuse by Proof Term Transformation
152
Proving Compatibility Using Refinement
168
Shallow Versus Deep Embedding
305
Term Algebras with Length Function and Bounded Quantifier Alternation
321
Author Index
337
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information