Theorem Proving in Higher Order Logics [[electronic resource] ] : 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings / / edited by Klaus Schneider, Jens Brandt
(Visualizza in formato marc)
(Visualizza in BIBFRAME)
| Titolo: |
Theorem Proving in Higher Order Logics [[electronic resource] ] : 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings / / edited by Klaus Schneider, Jens Brandt
|
| Pubblicazione: | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Edizione: | 1st ed. 2007. |
| Descrizione fisica: | 1 online resource (VIII, 404 p.) |
| Disciplina: | 005.115 |
| Soggetto topico: | Computer science |
| Machine theory | |
| Software engineering | |
| Artificial intelligence | |
| Logic design | |
| Theory of Computation | |
| Formal Languages and Automata Theory | |
| Computer Science Logic and Foundations of Programming | |
| Software Engineering | |
| Artificial Intelligence | |
| Logic Design | |
| Persona (resp. second.): | SchneiderKlaus <1967-> |
| BrandtJens <1978-> | |
| Note generali: | Bibliographic Level Mode of Issuance: Monograph |
| Nota di bibliografia: | Includes bibliographical references and index. |
| Nota di contenuto: | On the Utility of Formal Methods in the Development and Certification of Software -- Formal Techniques in Software Engineering: Correct Software and Safe Systems -- Separation Logic for Small-Step cminor -- Formalising Java’s Data Race Free Guarantee -- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL -- Formalising Generalised Substitutions -- Extracting Purely Functional Contents from Logical Inductive Types -- A Modular Formalisation of Finite Group Theory -- Verifying Nonlinear Real Formulas Via Sums of Squares -- Verification of Expectation Properties for Discrete Random Variables in HOL -- A Formally Verified Prover for the Description Logic -- Proof Pearl: The Termination Analysis of Terminator -- Improving the Usability of HOL Through Controlled Automation Tactics -- Verified Decision Procedures on Context-Free Grammars -- Using XCAP to Certify Realistic Systems Code: Machine Context Management -- Proof Pearl: De Bruijn Terms Really Do Work -- Proof Pearl: Looping Around the Orbit -- Source-Level Proof Reconstruction for Interactive Theorem Proving -- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF -- Automatically Translating Type and Function Definitions from HOL to ACL2 -- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models -- Proof Pearl: Wellfounded Induction on the Ordinals Up to ? 0 -- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols -- Primality Proving with Elliptic Curves -- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism -- Building Formal Method Tools in the Isabelle/Isar Framework -- Simple Types in Type Theory: Deep and Shallow Encodings -- Mizar’s Soft Type System. |
| Titolo autorizzato: | Theorem Proving in Higher Order Logics |
| ISBN: | 3-540-74591-2 |
| Formato: | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione: | Inglese |
| Record Nr.: | 996465287103316 |
| Lo trovi qui: | Univ. di Salerno |
| Opac: | Controlla la disponibilità qui |
Serie:
Theoretical Computer Science and General Issues, . 2512-2029 ; ; 4732