Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Theorem Proving in Higher Order Logics [[electronic resource] ] : 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings / / edited by Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan
| Theorem Proving in Higher Order Logics [[electronic resource] ] : 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings / / edited by Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (VIII, 340 p.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Computers Architecture, Computer Mathematical logic Computer logic Software engineering Artificial Intelligence Theory of Computation Computer System Implementation Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-30142-9 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNISA-996465430403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theorem Proving in Higher Order Logics : 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings / / edited by Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan
| Theorem Proving in Higher Order Logics : 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings / / edited by Konrad Slind, Annette Bunker, Ganesh C. Gopalakrishnan |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (VIII, 340 p.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Computers Architecture, Computer Mathematical logic Computer logic Software engineering Artificial Intelligence Theory of Computation Computer System Implementation Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering |
| ISBN | 3-540-30142-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNINA-9910144350603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||