Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, Volume 10
This 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.
Other editions - View all
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 expressions finite 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 Prolog proof normalization properties propositions protocol prove pseudo-functor queue quotients reasoning recursive refinement represent rewriting rules RUNWAY Section semantics sequence simulation specification language 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