Theorem Proving in Higher Order Logics 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Basin, David (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Wolff, Burkhart (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
• Έκδοση: 1st ed. 2003.
• Σειρά: Lecture Notes in Computer Science, 2758
• Θέματα: Philosophy.; Mathematical logic.; Logic design.; Software engineering.; Computer logic.; Artificial intelligence.; Philosophy, general.; Mathematical Logic and Formal Languages.; Logic Design.; Software Engineering.; Logics and Meanings of Programs.; Artificial Intelligence.

This volume constitutes the proceedings of the16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003) held September 8-12, 2003 in Rome, Italy. TPHOLs covers all aspects of theorem proving in higher order logics as well as related topics in theorem proving and veri?cati...

Πίνακας περιεχομένων:

• 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.