## Theorem Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, ProceedingsThis 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 |

Deﬁning Functions over Finite Sets | 385 |

Using Combinators to Manipulate letExpressions in Proof | 397 |

409 | |

### Other editions - View all

Theorem Proving in Higher Order Logics: 18th International Conference ... Joe Hurd,Tom Melham Limited preview - 2005 |

Theorem Proving in Higher Order Logics: 18th International Conference ... Joe Hurd No preview available - 2005 |

### Common terms and phrases

abs1 abs2 abstract ACL2 algorithm arithmetic arity axiom of choice axioms baseaddress bool Boolean Computer Science constdefs construct datatype define deﬁned definition denote derivation elements equality equivalence relation evaluation example expression extensionality fold1 formal formula function GeNoC Higher Order Logics higher-order logic implementation induction input instantiation Isabelle/HOL Java Java event spaces lazy theorem lemma levellist LNCS machine matrix Melham memory method model checking monad monad transformers multiset natural numbers nbblocks node nominal sets operations parameter partial equivalence relations path predicate primitive problem proof assistant proof obligations properties prove quotient recursive representation represented result rewrite RLTL rules semantics sequence specification Springer-Verlag structure subset syntax theorem prover theory tion TPHOLs translation type constructors UNCURRY valid variables verification VHDL well-founded relation