Theorem Proving in Higher Order Logics [electronic resource] : 12th International Conference, TPHOLs’ 99 Nice, France, September 14–17, 1999 Proceedings / edited by Yves Bertot, Gilles Dowek, Laurent Théry, André Hirschowitz, Christine Paulin.
Material type: TextSeries: Lecture Notes in Computer Science ; 1690Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999Description: VIII, 364 p. online resourceContent type: text Media type: computer Carrier type: online resourceISBN: 9783540482567Subject(s): Mathematics | Software engineering | Logic design | Computer science | Artificial intelligence | Computer software | Mathematics | Applications of Mathematics | Mathematical Software | Mathematical Logic and Formal Languages | Logics and Meanings of Programs | Artificial Intelligence (incl. Robotics) | Software EngineeringAdditional physical formats: Printed edition:: No titleDDC classification: 519 LOC classification: T57-57.97Online resources: Click here to access onlineCurrent library | Home library | Call number | Materials specified | URL | Status | Date due | Barcode |
---|---|---|---|---|---|---|---|
IMSc Library | IMSc Library | Link to resource | Available | EBK6391 |
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.