Theorem Proving in Higher Order Logics [electronic resource] : 12th International Conference, TPHOLs'99, Nice, France, September 14-17, 1999, Proceedings /
Material type: TextSeries: Lecture Notes in Computer Science ; 1690Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999Edition: 1st ed. 1999Description: VIII, 364 p. online resourceContent type:- text
- computer
- online resource
- 9783540482567
- 519 23
- T57-57.97
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.
There are no comments on this title.