Theorem proving in higher order logics : 14th international conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3 6, 2001 : proceedings
This volume constitutes the proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001) held 3 6 September 2001 in Edinburgh, Scotland. TPHOLs covers all aspects of theorem proving in higher order logics, as well as related topics in theorem proving and v...
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
2152 |
| 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, 14th international conference, TPHOLs 2001, Edinburgh, Scotland UK, September 3-6, 2001, proceedings, Richard J. Boulton, Paul B. Jackson (eds.), 2001, New York, Springer, 1 vol. (X-393 p.), Lecture notes in computer science, 3-540-42525-X • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662199183 |
Sommario:
- Invited Talks
- JavaCard Program Verification
- View from the Fringe of the Fringe
- Using Decision Procedures with a Higher-Order Logic
- Regular Contributions
- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
- An Irrational Construction of ? from ?
- HELM and the Semantic Math-Web
- Calculational Reasoning Revisited An Isabelle/Isar Experience
- Mechanical Proofs about a Non-repudiation Protocol
- Proving Hybrid Protocols Correct
- Nested General Recursion and Partiality in Type Theory
- A Higher-Order Calculus for Categories
- Certifying the Fast Fourier Transform with Coq
- A Generic Library for Floating-Point Numbers and Its Application to Exact Computing
- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain
- Abstraction and Refinement in Higher Order Logic
- A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL
- Representing Hierarchical Automata in Interactive Theorem Provers
- Refinement Calculus for Logic Programming in Isabelle/HOL
- Predicate Subtyping with Predicate Sets
- A Structural Embedding of Ocsid in PVS
- A Certified Polynomial-Based Decision Procedure for Propositional Logic
- Finite Set Theory in ACL2
- The HOL/NuPRL Proof Translator
- Formalizing Convex Hull Algorithms
- Experiments with Finite Tree Automata in Coq
- Mizar Light for HOL Light.