Theorem Proving in Higher Order Logics - Couverture souple

Couverture souple

ISBN 10 : 3662199483 ISBN 13 : 9783662199480

Editeur : Springer, 2014

Synopsis

Invited Talk I.- Click'n Prove: Interactive Proofs within Set Theory.- Hardware and Assembler Languages.- Formal Specification and Verification of ARM6.- A Programming Logic for Java Bytecode Programs.- Verified Bytecode Subroutines.- Proof Automation I.- Complete Integer Decision Procedures as Derived Rules in HOL.- Changing Data Representation within the Coq System.- Applications of Polytypism in Theorem Proving.- Proof Automation II.- A Coverage Checking Algorithm for LF.- Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions.- Tool Combination.- Embedding of Systems of Affine Recurrence Equations in Coq.- Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover.- Combining Testing and Proving in Dependent Type Theory.- Invited Talk II.- Reasoning about Proof Search Specifications: An Abstract.- Logic Extensions.- Program Extraction from Large Proof Developments.- First Order Logic with Domain Conditions.- Extending Higher-Order Unification to Support Proof Irrelevance.- Advances in Theorem Prover Technology.- Inductive Invariants for Nested Recursion.- Implementing Modules in the Coq System.- MetaPRL - A Modular Logical Environment.- Mathematical Theories.- Proving Pearl: Knuth's Algorithm for Prime Numbers.- Formalizing Hilbert's Grundlagen in Isabelle/Isar.- Security.- Using Coq to Verify Java CardTM Applet Isolation Properties.- Verifying Second-Level Security Protocols.

Détails de l'édition

• Éditeur: Springer
• Date d'édition: 2014
• Langue: anglais
• ISBN 10: 3662199483
• ISBN 13: 9783662199480
• Reliure: Broché
• Nombre de pages: 380
• Éditeur: Basin David, Wolff Burkhart
• Coordonnées du fabricant: KINESIS; https://www.also.com/ec/cms5/en_6000/6000/index.jsp; ; Friedrich-Karl-Str. 9; Hamburg; 22391; Allemagne