Theorem proving in higher order logics : 17th international conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004 : proceedings

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

Descripció completa

Guardat en:
Dades bibliogràfiques
Autor principal: Slind, Konrad
Autor corporatiu: International conference on theorem proving in higher order logics (Autor)
Altres autors: Bunker, Annette (Director editorial), Gopalakrishnan, Ganesh (Director editorial)
Format: Livre numérique
Idioma:Anglais
Publicat: Berlin [etc.] : Springer [20..].
Cham : Springer Nature
Col·lecció:Lecture notes in computer science 3223
Matèries:
Génie logiciel
Informatique
Intelligence artificielle
Logique symbolique et mathématique
Théorèmes > Démonstration automatique
Structure logique
Actes de congrès
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, 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
Taula de continguts:
  • 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.

Ítems similars