Theorem proving in higher order logics : 12th international conference, TPHOLs '99, Nice, France, September 14-17, 1999 : proceedings
Uloženo v:
| Korporativní autor: | |
|---|---|
| Další autoři: | , , |
| Médium: | Livre numérique |
| Jazyk: | Anglais |
| Vydáno: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Edice: | Lecture notes in computer science
1690 |
| Témata: | |
| On-line přístup: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Poznámka: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Theorem proving in higher order logics, 12th international conference, TPHOLs '99, Nice, France, September 14-17, 1999, proceedings, Yves Bertot ... [et al.], eds, 1999, Berlin, Springer, 1 vol. (VIII-358 p.), Lecture notes in computer science, 3-540-66463-7 • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662183410 |
Obsah:
- 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.