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 /
TPHOLs 2004
editors, Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan.
- Berlin : Springer, 2004.
- 1 online resource (viii, 336 pages) : illustrations
- Lecture notes in computer science ; 3223 .
- Lecture notes in computer science ; 3223. .
Title from title screen (viewed December 10, 2004). Print version originally published in 2004.
Includes bibliographical references and index.
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.
This book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA, in September 2004. The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction.
3540301429 9783540301424 9788354030140 8354030148
10.1007/b100400 doi
97200064X DE-101
Automatic theorem proving--Congresses.
Théorèmes--Démonstration automatique--Congrès.
COMPUTERS--Expert Systems.
Automatic theorem proving
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
QA76.9.A96 / T655 2004eb
006.333
Title from title screen (viewed December 10, 2004). Print version originally published in 2004.
Includes bibliographical references and index.
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.
This book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA, in September 2004. The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction.
3540301429 9783540301424 9788354030140 8354030148
10.1007/b100400 doi
97200064X DE-101
Automatic theorem proving--Congresses.
Théorèmes--Démonstration automatique--Congrès.
COMPUTERS--Expert Systems.
Automatic theorem proving
proceedings (reports)
Conference papers and proceedings
Conference papers and proceedings.
Actes de congrès.
QA76.9.A96 / T655 2004eb
006.333