Theorem proving in higher order logics : 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004 : proceedings
This volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14 17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higher-order logics as well as related topics in theorem proving an...
Zapisane w:
| 1. autor: | |
|---|---|
| Korporacja: | |
| Kolejni autorzy: | , |
| Format: | Livre numérique |
| Język: | Anglais |
| Wydane: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Seria: | Lecture notes in computer science
3223 |
| Hasła przedmiotowe: | |
| Dostęp 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 |
| Komentarz: |
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, 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, proceedings, Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.), Berlin, Springer, 2004, 1 vol. (VIII-336 p.), Lecture notes in computer science, 3-540-23017-3 • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662211625 |
| LEADER | 05166nam a22004457a 4500 | ||
|---|---|---|---|
| 001 | 971657 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155210661 | ||
| 020 | |a 9783540301424 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 100 | 1 | |a Slind, Konrad. | |
| 245 | 1 | 0 | |a Theorem proving in higher order logics : |b 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004 : proceedings |c [edited by] Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 3223 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Error Analysis of Digital Filters Using Theorem Proving -- Verifying Uniqueness in a Logical Framework -- A Program Logic for Resource Verification -- Proof Reuse with Extended Inductive Types -- Hierarchical Reflection -- Correct Embedded Computing Futures -- Higher Order Rippling in IsaPlanner -- A Mechanical Proof of the Cook-Levin Theorem -- Formalizing the Proof of the Kepler Conjecture -- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code -- Extensible Hierarchical Tactic Construction in a Logical Framework -- Theorem Reuse by Proof Term Transformation -- Proving Compatibility Using Refinement -- Java Program Verification via a JVM Deep Embedding in ACL2 -- Reasoning About CBV Functional Programs in Isabelle/HOL -- Proof Pearl: From Concrete to Functional Unparsing -- A Decision Procedure for Geometry in Coq -- Recursive Function Definition for Types with Binders -- Abstractions for Fault-Tolerant Distributed System Verification -- Formalizing Integration Theory with an Application to Probabilistic Algorithms -- Formalizing Java Dynamic Loading in HOL -- Certifying Machine Code Safety: Shallow Versus Deep Embedding -- Term Algebras with Length Function and Bounded Quantifier Alternation. | |
| 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 | ||
| 520 | |a This volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14 17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higher-order logics as well as related topics in theorem proving and veri?cation. There were 42 papers submitted to TPHOLs 2004 in the full research ca- gory, each of which was refereed by at least 3 reviewers selected by the program committee. Of these submissions, 21 were accepted for presentation at the c- ference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2004 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings c- taining papers about in-progress work was published as a 2004 technical report of the School of Computing at the University of Utah. The organizers are grateful to Al Davis, Thomas Hales, and Ken McMillan for agreeing to give invited talks at TPHOLs 2004. The TPHOLs conference traditionally changes continents each year in order to maximize the chances that researchers from around the world can attend. | ||
| 650 | |a Génie logiciel | ||
| 650 | |a Informatique | ||
| 650 | |a Intelligence artificielle | ||
| 650 | |a Logique symbolique et mathématique | ||
| 650 | |a Théorèmes |x Démonstration automatique | ||
| 650 | |a Structure logique | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Bunker, Annette. |4 pbd | |
| 700 | 1 | |a Gopalakrishnan, Ganesh. |4 pbd | |
| 711 | 2 | |a International conference on theorem proving in higher order logics |n (17 |d :2004 |c :Park City, Utah). |4 aut | |
| 776 | 0 | |0 083250891 |t Theorem proving in higher order logics |o 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004 |o proceedings |f Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.) |c Berlin |n Springer |d 2004 |p 1 vol. (VIII-336 p.) |s Lecture notes in computer science |z 3-540-23017-3 | |
| 776 | 0 | |t Theorem Proving in Higher Order Logics |b Texte imprimé |z 9783662211625 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/b100400 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-J6TVC9JN-Q |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:750650168 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/b100400 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:754000664 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/b100400 |z Accès INSA CVL | |
| 997 | |0 971657 |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/ | ||