## Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, ProceedingsThis book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '98, held in Canberra, Australia, in September/October 1998. The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed. |

### What people are saying - Write a review

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

### Contents

I | 1 |

II | 17 |

III | 33 |

IV | 49 |

V | 67 |

VI | 87 |

VII | 105 |

VIII | 123 |

XVI | 263 |

XVII | 277 |

XVIII | 295 |

XIX | 315 |

XX | 331 |

XXI | 349 |

XXII | 367 |

XXIII | 387 |

IX | 143 |

X | 153 |

XI | 171 |

XII | 189 |

XIII | 207 |

XIV | 225 |

XV | 245 |

XXIV | 401 |

XXV | 423 |

XXVI | 443 |

XXVII | 461 |

XXVIII | 479 |

XXIX | |

### Other editions - View all

Theorem Proving in Higher Order Logics: 11th International Conference ... Jim Grundy,Malcolm Newey No preview available - 2014 |

Theorem Proving in Higher Order Logics: 11th International Conference ... Jim Grundy,Malcolm Newey No preview available - 2005 |

### Common terms and phrases

abstract algorithm annotations applied argument assumptions Automated automatically axiomatization bool CLAM co-inductive Computer Science concrete construct constructors context correctness corresponding dart data refinement decision procedures defined definition defs denoted derived domain encoding environment example expression finite first-order first-order logic formal assertions formal verification formula free maps free variables function goal graph Higher Order Logic higher-order logic hypothesis implementation induction inference rules instantiation Isabelle Isabelle/HOL Lecture Notes lemmas loop meta-logic methods model checking natural deduction node Notes in Computer Nuprl operator outv pair path predicate programming language proof systems proof tool properties propositional provability prove quantified quasi-maps recursive register allocation relation relevant logics result rewriting satisfies Sect semantics sequent calculus Springer-Verlag step structure subderivation subgoals subterm syntax tactics term termination ternary relations theorem prover transformation transition translation verification conditions window inference