## Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, ProceedingsThis book constitutes the refereed proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '97, held in Murray Hill, NJ, USA, in August 1997. The volume presents 19 carefully revised full papers selected from 32 submissions during a thorough reviewing process. The papers cover work related to all aspects of theorem proving in higher order logics, particularly based on secure mechanization of those logics; the theorem proving systems addressed include Coq, HOL, Isabelle, LEGO, and PVS. |

### What people are saying - Write a review

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

### Contents

An IsabelleBased Theorem Prover for VDMSL | 1 |

Executing Formal Specifications by Translation to Higher Order Logic | 17 |

HumanStyle Theorem Proving Using | 33 |

Copyright | |

14 other sections not shown

### Other editions - View all

### Common terms and phrases

7r-calculus abstract action systems algorithm andthen application automatically automation axioms bicategory bisimulation bool boolean calculus category theory circuit class schema components Computer Science construct conversion step datatype decision procedures defined derived described domain embedding encoding equivalence relation example finite first-order logic formal proof formal verification function goal higher order logic higher-order logic human-style implementation induction theorem input instantiation Isabelle Isabelle/HOL Lambda Prolog LEGO lemmas mechanism method model checking natural numbers notation object-oriented objects operator poly polynomial predicate Proceedings Prolog proof normalization properties propositions protocol prove pseudo-functor queue quotients reasoning recursive refinement represent rewriting rules Runway Section semantics sequence simulation strategy structural induction structure subgoal subtyping syntactic syntax tactics theorem prover tion tool trace transactions transition translation type classes type constructor type theory variables VDM-LPF VDM-SL verification Yoneda Yoneda embedding