product iamge

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

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Download
Search on Amazon

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

THis book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA in September 2004.

The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction.

Author(s): Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan
Series: Lecture notes in computer science 3223
Publisher: Springer
Year: 2004

Language: English
Pages: 349

Table of Contents......Page 8
Error Analysis of Digital Filters Using Theorem Proving......Page 10
Verifying Uniqueness in a Logical Framework......Page 27
A Program Logic for Resource Verification......Page 43
Proof Reuse with Extended Inductive Types......Page 59
Hierarchical Reflection......Page 75
Correct Embedded Computing Futures......Page 91
Higher Order Rippling in ISAPLANNER......Page 92
A Mechanical Proof of the Cook-Levin Theorem......Page 108
Formalizing the Proof of the Kepler Conjecture......Page 126
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code......Page 127
Extensible Hierarchical Tactic Construction in a Logical Framework......Page 145
Theorem Reuse by Proof Term Transformation......Page 161
Proving Compatibility Using Refinement......Page 177
Java Program Verification via a JVM Deep Embedding in ACL2......Page 193
Reasoning About CBV Functional Programs in Isabelle/HOL......Page 210
Proof Pearl: From Concrete to Functional Unparsing......Page 226
A Decision Procedure for Geometry in Coq......Page 234
Recursive Function Definition for Types with Binders......Page 250
Abstractions for Fault-Tolerant Distributed System Verification......Page 266
Formalizing Integration Theory with an Application to Probabilistic Algorithms......Page 280
Formalizing Java Dynamic Loading in HOL......Page 296
Certifying Machine Code Safety: Shallow Versus Deep Embedding......Page 314
Term Algebras with Length Function and Bounded Quantifier Alternation......Page 330
Author Index......Page 346