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

Front Cover
Springer Science & Business Media, Aug 8, 2005 - Computers - 408 pages
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.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

On the Correctness of Operating System Kernels
1
AlphaStructural Recursion and Induction
17
Shallow Lazy Proofs
35
The PoplMark Challenge
50
A Structured Set of HigherOrder Problems
66
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
82
Proving Equalities in a Commutative Ring Done Right in Coq
98
A HOL Theory of Euclidean Space
114
Proving Bounds for Real Linear Programs in IsabelleHOL
227
Essential Incompleteness of Arithmetic Verified by Coq
245
Verification of BDD Normalization
261
Extensionality in the Calculus of Constructions
278
A Mechanically Verified Sound and Complete Theorem Prover for First Order Logic
294
A Generic Network on Chip Model
310
Using ACL2
326
A Formal Validation in HOL
342

A Design Structure for Higher Order Quotients
130
Axiomatic Constructor Classes in IsabelleHOLCF
147
Meta Reasoning in ACL2
163
Reasoning About Java Programs with Aliasing and Frame Conditions
179
Real Number Calculations and Theorem Proving
195
Verifying a Secure Information Flow Analyzer
211
A Formal Proof of Higmans Lemma in ACL2
358
Dijkstras Shortest Path Algorithm Verified with ACL2
373
Defining Functions over Finite Sets
385
Using Combinators to Manipulate letExpressions in Proof
397
Author Index
409
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information