03063oam 2200553 450 991014364830332120210715224018.03-540-48256-310.1007/3-540-48256-3(CKB)1000000000211140(SSID)ssj0000327170(PQKBManifestationID)11230126(PQKBTitleCode)TC0000327170(PQKBWorkID)10301593(PQKB)11045240(DE-He213)978-3-540-48256-7(MiAaPQ)EBC3073024(MiAaPQ)EBC6485865(PPN)155230301(EXLCZ)99100000000021114020210715d1999 uy 0engurnn|008mamaatxtccrTheorem proving in higher order logics 12th international conference, TPHOLs '99, Nice, France, September 14-17, 1999 : proceedings /Yves Bertot [and four others], editors1st ed. 1999.Berlin ;Heidelberg :Springer,[1999]©19991 online resource (VIII, 364 p.) Lecture Notes in Computer Science ;1690Bibliographic Level Mode of Issuance: Monograph3-540-66463-7 Includes bibliographical references at the end of each chapters and index.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.Lecture notes in computer science ;1690.Automatic theorem provingCongressesAutomatic theorem proving004.015113Bertot YvesTPHOLs '99MiAaPQMiAaPQUtOrBLWBOOK9910143648303321Theorem Proving in Higher Order Logics772309UNINA