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.

Por: Schneider, Klaus [editor.]Colaborador(es): Brandt, Jens [editor.]Tipo de material: TextoTextoSeries Lecture Notes in Computer Science, 4732Editor: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007Descripción: VIII, 404 p. online resourceTipo de contenido: text Tipo de medio: computer Tipo de portador: online resourceISBN: 9783540745914Trabajos contenidos: SpringerLink (Online service)Tema(s): Computer science | Logic design | Software engineering | Artificial intelligence | Computer Science | Mathematical Logic and Formal Languages | Logics and Meanings of Programs | Software Engineering | Artificial Intelligence (incl. Robotics) | Logic DesignFormatos físicos adicionales: Sin títuloClasificación CDD: 005.131 Clasificación LoC:QA8.9-QA10.3Recursos en línea: de clik aquí para ver el libro electrónico
Contenidos:
Springer eBooks
Etiquetas de esta biblioteca: No hay etiquetas de esta biblioteca para este título. Ingresar para agregar etiquetas.
    Valoración media: 0.0 (0 votos)
No hay ítems correspondientes a este registro

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 Javas 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: DeBruijn 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 -- Mizars Soft Type System.

ZDB-2-SCS

ZDB-2-LNC

No hay comentarios en este titulo.

para colocar un comentario.