Theorem proving in higher order logics : 16th international conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003 : proceedings
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...
Salvato in:
| Ente Autore: | |
|---|---|
| Altri autori: | , |
| Natura: | Livre numérique |
| Lingua: | Anglais |
| Pubblicazione: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serie: | Lecture notes in computer science
2758 |
| Soggetti: | |
| Accesso online: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
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, 16th international conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003, proceedings, David Basin, Burkhart Wolff (eds.), Berlin, Springer, 2003, 1 vol. (X-366 p.), Lecture notes in computer science, 3-540-40664-6 • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662199480 |
Sommario:
- 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.