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.
Author(s): Behzad Akbarpour, Sofiène Tahar (auth.), Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.)
Series: Lecture Notes in Computer Science 3223
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2004
Language: English
Pages: 340
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering; Artificial Intelligence (incl. Robotics); Logic Design
Front Matter....Pages -
Error Analysis of Digital Filters Using Theorem Proving....Pages 1-17
Verifying Uniqueness in a Logical Framework....Pages 18-33
A Program Logic for Resource Verification....Pages 34-49
Proof Reuse with Extended Inductive Types....Pages 50-65
Hierarchical Reflection....Pages 66-81
Correct Embedded Computing Futures....Pages 82-82
Higher Order Rippling in IsaPlanner ....Pages 83-98
A Mechanical Proof of the Cook-Levin Theorem....Pages 99-116
Formalizing the Proof of the Kepler Conjecture....Pages 117-117
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code....Pages 118-135
Extensible Hierarchical Tactic Construction in a Logical Framework....Pages 136-151
Theorem Reuse by Proof Term Transformation....Pages 152-167
Proving Compatibility Using Refinement....Pages 168-183
Java Program Verification via a JVM Deep Embedding in ACL2....Pages 184-200
Reasoning About CBV Functional Programs in Isabelle/HOL....Pages 201-216
Proof Pearl: From Concrete to Functional Unparsing....Pages 217-224
A Decision Procedure for Geometry in Coq....Pages 225-240
Recursive Function Definition for Types with Binders....Pages 241-256
Abstractions for Fault-Tolerant Distributed System Verification....Pages 257-270
Formalizing Integration Theory with an Application to Probabilistic Algorithms....Pages 271-286
Formalizing Java Dynamic Loading in HOL....Pages 287-304
Certifying Machine Code Safety: Shallow Versus Deep Embedding....Pages 305-320
Term Algebras with Length Function and Bounded Quantifier Alternation....Pages 321-336
Back Matter....Pages -
