E-Book, Englisch, Band 1690, 364 Seiten, eBook
Bertot / Dowek / Hirschowitz Theorem Proving in Higher Order Logics
1999
ISBN: 978-3-540-48256-7
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
12th International Conference, TPHOLs'99, Nice, France, September 14-17, 1999, Proceedings
E-Book, Englisch, Band 1690, 364 Seiten, eBook
Reihe: Lecture Notes in Computer Science
ISBN: 978-3-540-48256-7
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Zielgruppe
Research
Autoren/Hrsg.
Weitere Infos & Material
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.
