Theorem Proving in Higher Order Logics : 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings / edited by Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan.

Format:

Book

Contributor:

Slind, Konrad, editor.

Bunker, Annette, editor.

Gopalakrishnan, Ganesh C., editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science 0302-9743 ; 3223.

Lecture Notes in Computer Science, 0302-9743 ; 3223

Language:

English

Subjects (All):

Artificial intelligence.

Computers.

Computer architecture.

Logic, Symbolic and mathematical.

Computer logic.

Software engineering.

Artificial Intelligence.

Theory of Computation.

Computer System Implementation.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Local Subjects:

Artificial Intelligence.

Theory of Computation.

Computer System Implementation.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Physical Description:

1 online resource (VIII, 340 pages).

Edition:

First edition 2004.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.

System Details:

text file PDF

Summary:

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.

Contents:

Error Analysis of Digital Filters Using Theorem Proving

Verifying Uniqueness in a Logical Framework

A Program Logic for Resource Verification

Proof Reuse with Extended Inductive Types

Hierarchical Reflection

Correct Embedded Computing Futures

Higher Order Rippling in IsaPlanner

A Mechanical Proof of the Cook-Levin Theorem

Formalizing the Proof of the Kepler Conjecture

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

Extensible Hierarchical Tactic Construction in a Logical Framework

Theorem Reuse by Proof Term Transformation

Proving Compatibility Using Refinement

Java Program Verification via a JVM Deep Embedding in ACL2

Reasoning About CBV Functional Programs in Isabelle/HOL

Proof Pearl: From Concrete to Functional Unparsing

A Decision Procedure for Geometry in Coq

Recursive Function Definition for Types with Binders

Abstractions for Fault-Tolerant Distributed System Verification

Formalizing Integration Theory with an Application to Probabilistic Algorithms

Formalizing Java Dynamic Loading in HOL

Certifying Machine Code Safety: Shallow Versus Deep Embedding

Term Algebras with Length Function and Bounded Quantifier Alternation.

Other Format:

Printed edition:

ISBN:

978-3-540-30142-4

9783540301424

Access Restriction:

Restricted for use by site license.