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.
Author(s): Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, Wolfgang Paul (auth.), Joe Hurd, Tom Melham (eds.)
Series: Lecture Notes in Computer Science 3603 : Theoretical Computer Science and General Issues
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 414
Tags: Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering; Artificial Intelligence (incl. Robotics); Logic Design
Front Matter....Pages -
On the Correctness of Operating System Kernels....Pages 1-16
Alpha-Structural Recursion and Induction....Pages 17-34
Shallow Lazy Proofs....Pages 35-49
Mechanized Metatheory for the Masses: The P opl M ark Challenge....Pages 50-65
A Structured Set of Higher-Order Problems....Pages 66-81
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS....Pages 82-97
Proving Equalities in a Commutative Ring Done Right in Coq....Pages 98-113
A HOL Theory of Euclidean Space....Pages 114-129
A Design Structure for Higher Order Quotients....Pages 130-146
Axiomatic Constructor Classes in Isabelle/HOLCF....Pages 147-162
Meta Reasoning in ACL2....Pages 163-178
Reasoning About Java Programs with Aliasing and Frame Conditions....Pages 179-194
Real Number Calculations and Theorem Proving....Pages 195-210
Verifying a Secure Information Flow Analyzer....Pages 211-226
Proving Bounds for Real Linear Programs in Isabelle/HOL....Pages 227-244
Essential Incompleteness of Arithmetic Verified by Coq....Pages 245-260
Verification of BDD Normalization....Pages 261-277
Extensionality in the Calculus of Constructions....Pages 278-293
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic....Pages 294-309
A Generic Network on Chip Model....Pages 310-325
Formal Verification of a SHA-1 Circuit Core Using ACL2....Pages 326-341
From PSL to LTL: A Formal Validation in HOL....Pages 342-357
Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2....Pages 358-372
Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2....Pages 373-384
Proof Pearl: Defining Functions over Finite Sets....Pages 385-396
Proof Pearl: Using Combinators to Manipulate let -Expressions in Proof....Pages 397-408
Back Matter....Pages -
