Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99, Nice, France, September 14-17, 1999, Proceedings: Lecture Notes in Computer Science, cartea 1690

Recent Advancements in Hardware Verification — How to Make Theorem Proving Fit for an Industrial Usage.- Disjoint Sums over Type Classes in HOL.- Inductive Datatypes in HOL — Lessons Learned in Formal-Logic Engineering.- Isomorphisms — A Link Between the Shallow and the Deep.- Polytypic Proof Construction.- Recursive Function Definition over Coinductive Types.- Hardware Verification Using Co-induction in COQ.- Connecting Proof Checkers and Computer Algebra Using OpenMath.- A Machine-Checked Theory of Floating Point Arithmetic.- Universal Algebra in Type Theory.- Locales A Sectioning Concept for Isabelle.- Isar — A Generic Interpretative Approach to Readable Formal Proof Documents.- On the Implementation of an Extensible Declarative Proof Language.- Three Tactic Theorem Proving.- Mechanized Operational Semantics via (Co)Induction.- Representing WP Semantics in Isabelle/ZF.- A HOL Conversion for Translating Linear Time Temporal Logic to ?-Automata.- From I/O Automata to Timed I/O Automata.- Formal Methods and Security Evaluation.- Importing MDG Verification Results into HOL.- Integrating Gandalf and HOL.- Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving.- Symbolic Functional Evaluation.

Includes supplementary material: sn.pub/extras