Theorem Proving in Higher Order Logics : 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings,9783540283720

Theorem Proving in Higher Order Logics : 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings

by ;
ISBN13: 9783540283720
ISBN10: 3540283722
Format: Paperback
Pub. Date: 2005-10-16
Publisher(s): Springer Verlag
  • Free Shipping Icon

    This Item Qualifies for Free Shipping!*

    *Excludes marketplace orders.

List Price: $124.95

Rent Textbook

Select for Price
Add to Cart
There was a problem. Please try again later.

New Textbook

We're Sorry
Sold Out

Used Textbook

We're Sorry
Sold Out

eTextbook

We're Sorry
Not Available

Buy from our Marketplace starting at $21.81

How Marketplace Works:

  • This item is offered by an independent seller and not shipped from our warehouse
  • Item details like edition and cover design may differ from our description; see seller's comments before ordering.
  • Sellers much confirm and ship within two business days; otherwise, the order will be cancelled and refunded.
  • Marketplace purchases cannot be returned to eCampus.com. Contact the seller directly for inquiries; if no response within two days, contact customer service.
  • Additional shipping costs apply to Marketplace purchases. Review shipping costs at checkout.

Summary

This book constitutes the refereed proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005, held in Oxford, UK, in August 2005. The 20 revised full papers presented together with 2 invited papers and 4 proof pearls (concise and elegant presentations of interesting examples) were carefully reviewed and selected from 49 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the topics of this volume are theorem proving, verification, recursion and induction, mechanized proofs, mathematical logic, proof theory, type systems, program verification, and proving systems like HOL, Coq, ACL2, Isabelle/HOL and Isabelle/HOLCF.

Table of Contents

Invited Papers
On the Correctness of Operating System Kernels
Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, Wolfgang Paul
1(16)
Alpha-Structural Recursion and Induction
Andrew M. Pitts
17(18)
Regular Papers
Shallow Lazy Proofs
Hasan Amjad
35(15)
Mechanized Metatheory for the Masses: The POPLMARK Challenge
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic
50(16)
A Structured Set of Higher-Order Problems
Christoph E. Benzmüller, Chad E. Brown
66(16)
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
Néstor Cataño
82(16)
Proving Equalities in a Commutative Ring Done Right in Coq
Benjamin Grégoire, Assia Mahboubi
98(16)
A HOL Theory of Euclidean Space
John Harrison
114(16)
A Design Structure for Higher Order Quotients
Peter V. Homeier
130(17)
Axiomatic Constructor Classes in Isabelle/HOLCF
Brian Huffman, John Matthews, Peter White
147(16)
Meta Reasoning in ACL2
Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
163(16)
Reasoning About Java Programs with Aliasing and Frame Conditions
Claude Marché, Christine Paulin-Mohring
179(16)
Real Number Calculations and Theorem Proving
César Muñoz, David Lester
195(16)
Verifying a Secure Information Flow Analyzer
David A. Naumann
211(16)
Proving Bounds for Real Linear Programs in Isabelle/HOL
Steven Obua
227(18)
Essential Incompleteness of Arithmetic Verified by Coq
Russell O'Connor
245(16)
Verification of BDD Normalization
Veronika Ortner, Norbert Schirmer
261(17)
Extensionality in the Calculus of Constructions
Nicolas Oury
278(16)
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
Tom Ridge, James Margetson
294(16)
A Generic Network on Chip Model
Julien Schmaltz, Dominique Borrione
310(16)
Formal Verification of a SHA-1 Circuit Core Using ACL2
Diana Toma, Dominique Borrione
326(16)
From PSL to LTL: A Formal Validation in HOL
Thomas Tuerk, Klaus Schneider
342(16)
Proof Pearls
Proof Pearl: A Formal Proof of Higman's Lemma in ACL
L2
Francisco J. Martin-Mateos, José L. Ruiz-Reina, José A. Alonso, Maria J. Hidalgo
358(15)
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2
J Strother Moore, Qiang Zhang
373(12)
Proof Pearl: Defining Functions over Finite Sets
Tobias Nipkow, Lawrence C. Paulson
385(12)
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof
Michael Norrish, Konrad Slind
397(12)
Author Index 409

An electronic version of this book is available through VitalSource.

This book is viewable on PC, Mac, iPhone, iPad, iPod Touch, and most smartphones.

By purchasing, you will be able to view this book online, as well as download it, for the chosen number of days.

Digital License

You are licensing a digital product for a set duration. Durations are set forth in the product description, with "Lifetime" typically meaning five (5) years of online access and permanent download to a supported device. All licenses are non-transferable.

More details can be found here.

A downloadable version of this book is available through the eCampus Reader or compatible Adobe readers.

Applications are available on iOS, Android, PC, Mac, and Windows Mobile platforms.

Please view the compatibility matrix prior to purchase.