| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910143648303321 |
|
|
Titolo |
Theorem proving in higher order logics : 12th international conference, TPHOLs '99, Nice, France, September 14-17, 1999 : proceedings / / Yves Bertot [and four others], editors |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin ; ; Heidelberg : , : Springer, , [1999] |
|
©1999 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1999.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VIII, 364 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science ; ; 1690 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Automatic theorem proving |
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references at the end of each chapters and index. |
|
|
|
|
|
|
|
|
Nota di contenuto |
|
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. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNISA996483160903316 |
|
|
Titolo |
Computational science and its applications - ICCSA 2022 workshops . Part III : Malaga, Spain, July 4-7, 2022, proceedings / / Osvaldo Gervasi [and four others], editors |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham, Switzerland : , : Springer Nature Switzerland AG, , [2022] |
|
©2022 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Descrizione fisica |
|
1 online resource (733 pages) |
|
|
|
|
|
|
Collana |
|
Lecture notes in computer science ; ; 13379 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computer science |
Computer networks |
Computer software |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
| |