Theorem Proving in Higher Order Logics : 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20 23, 2002 Proceedings
Guardat en:
| Autor corporatiu: | |
|---|---|
| Altres autors: | , , |
| Format: | Livre numérique |
| Idioma: | Anglais |
| Publicat: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Col·lecció: | Lecture notes in computer science
2410 |
| Matèries: | |
| Accés en línia: | 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, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, proceedings, Victor A. Carreño, César A. Muñoz, Sofiène Tahar, eds, Berlin, Springer, 2002, 1 vol. (X-347 p.), Lecture notes in computer science, 3-540-44039-9 • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662182413 |
| LEADER | 03771nam a22004097a 4500 | ||
|---|---|---|---|
| 001 | 948995 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155204688 | ||
| 020 | |a 9783540456858 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 111 | 2 | |a International conference on theorem proving in higher order logics |n (15 |d :2002 |c :Hampton, Va.). | |
| 245 | 1 | 0 | |a Theorem Proving in Higher Order Logics : |b 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20 23, 2002 Proceedings |c edited by Victor A. Carreño, César A. Muñoz, Sofiène Tahar. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 2410 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Invited Talks -- Formal Methods at NASA Langley -- Higher Order Unification 30 Years Later -- Regular Papers -- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction -- Efficient Reasoning about Executable Specifications in Coq -- Verified Bytecode Model Checkers -- The 5 Colour Theorem in Isabelle/Isar -- Type-Theoretic Functional Semantics -- A Proposal for a Formal OCL Semantics in Isabelle/HOL -- Explicit Universes for the Calculus of Constructions -- Formalised Cut Admissibility for Display Logic -- Formalizing the Trading Theorem for the Classification of Surfaces -- Free-Style Theorem Proving -- A Comparison of Two Proof Critics: Power vs. Robustness -- Two-Level Meta-reasoning in Coq -- PuzzleTool: An Example of Programming Computation and Deduction -- A Formal Approach to Probabilistic Termination -- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm -- Quotient Types: A Modular Approach -- Sequent Schema for Derived Rules -- Algebraic Structures and Dependent Records -- Proving the Equivalence of Microstep and Macrostep Semantics -- Weakest Precondition for General Recursive Programs Formalized in Coq. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 650 | |a Génie logiciel | ||
| 650 | |a Informatique | ||
| 650 | |a Théorèmes |x Démonstration automatique | ||
| 650 | |a Structure logique | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Carreño, Victor A., |d 1956- |4 pbd | |
| 700 | 1 | |a Muñoz, César. |4 pbd | |
| 700 | 1 | |a Tahar, Sofiène. |4 pbd | |
| 776 | 0 | |0 069791163 |t Theorem proving in higher order logics |o 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002 |o proceedings |f Victor A. Carreño, César A. Muñoz, Sofiène Tahar, eds |c Berlin |n Springer |d 2002 |p 1 vol. (X-347 p.) |s Lecture notes in computer science |z 3-540-44039-9 | |
| 776 | 0 | |t Theorem Proving in Higher Order Logics |b Texte imprimé |z 9783662182413 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-45685-6 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-L47GNHB7-1 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:748057641 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-45685-6 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:751509027 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-45685-6 |z Accès INSA CVL | |
| 997 | |0 948995 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||