FEEDBACK Smiley face
Normal view MARC view ISBD view

Theorem Proving in Higher Order Logics [electronic resource] :12th International Conference, TPHOLs’ 99 Nice, France, September 14–17, 1999 Proceedings /

Contributor(s): Bertot, Yves [editor.] | Dowek, Gilles [editor.] | Théry, Laurent [editor.] | Hirschowitz, André [editor.] | Paulin, Christine [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Lecture Notes in Computer Science: 1690Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.Description: VIII, 364 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540482567.Subject(s): Mathematics | Software engineering | Computer logic | Mathematical logic | Artificial intelligence | Applied mathematics | Engineering mathematics | Computer software | Mathematics | Applications of Mathematics | Mathematical Software | Mathematical Logic and Formal Languages | Logics and Meanings of Programs | Artificial Intelligence (incl. Robotics) | Software EngineeringOnline resources: Click here to access online
Contents:
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.
In: Springer eBooks
Tags from this library: No tags from this library for this title. Add tag(s)
Log in to add tags.
    average rating: 0.0 (0 votes)
No physical items for this record

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 for this item.

Log in to your account to post a comment.

© IIIT-Delhi, 2013 | Phone: +91-11-26907510| FAX +91-11-26907405 | E-mail: library@iiitd.ac.in