Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings
Elsa L. Gunter, Amy Felty
Springer, Sep 12, 1997 - Computers - 339 pages
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.
An IsabelleBased Theorem Prover for VDMSL
Executing Formal Specifications by Translation to Higher Order Logic
HumanStyle Theorem Proving Using
14 other sections not shown
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 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