Theorem Proving in Higher Order Logics : 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings / edited by Joe Hurd, Tom Melham.

Format:

Book

Contributor:

Hurd, Joe, editor.

Melham, T. F. (Tom F.), editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

LNCS sublibrary. Theoretical computer science and general issues ; SL 1, 3603.

Theoretical Computer Science and General Issues ; 3603

Language:

English

Subjects (All):

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.

Artificial Intelligence.

Local Subjects:

Theory of Computation.

Computer System Implementation.

Mathematical Logic and Formal Languages.

Logics and Meanings of Programs.

Software Engineering.

Artificial Intelligence.

Physical Description:

1 online resource (X, 414 pages).

Edition:

First edition 2005.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2005.

System Details:

text file PDF

Summary:

This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22-25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 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 volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005.

Contents:

Invited Papers

On the Correctness of Operating System Kernels

Alpha-Structural Recursion and Induction

Regular Papers

Shallow Lazy Proofs

Mechanized Metatheory for the Masses: The PoplMark Challenge

A Structured Set of Higher-Order Problems

Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS

Proving Equalities in a Commutative Ring Done Right in Coq

A HOL Theory of Euclidean Space

A Design Structure for Higher Order Quotients

Axiomatic Constructor Classes in Isabelle/HOLCF

Meta Reasoning in ACL2

Reasoning About Java Programs with Aliasing and Frame Conditions

Real Number Calculations and Theorem Proving

Verifying a Secure Information Flow Analyzer

Proving Bounds for Real Linear Programs in Isabelle/HOL

Essential Incompleteness of Arithmetic Verified by Coq

Verification of BDD Normalization

Extensionality in the Calculus of Constructions

A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic

A Generic Network on Chip Model

Formal Verification of a SHA-1 Circuit Core Using ACL2

From PSL to LTL: A Formal Validation in HOL

Proof Pearls

Proof Pearl: A Formal Proof of Higman's Lemma in ACL2

Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2

Proof Pearl: Defining Functions over Finite Sets

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.

Other Format:

Printed edition:

ISBN:

978-3-540-31820-0

9783540318200

Access Restriction:

Restricted for use by site license.