17. TPHOLs 2004: Park City, Utah, USA

• Behzad Akbarpour, Sofiène Tahar:
  Error Analysis of Digital Filters Using Theorem Proving. 1-17
  
• Penny Anderson, Frank Pfenning:
  Verifying Uniqueness in a Logical Framework. 18-33
  
• David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, Alberto Momigliano:
  A Program Logic for Resource Verification. 34-49
  
• Olivier Boite:
  Proof Reuse with Extended Inductive Types. 50-65
  
• Luís Cruz-Filipe, Freek Wiedijk:
  Hierarchical Reflection. 66-81
  
• Al Davis:
  Correct Embedded Computing Futures. 82
  
• Lucas Dixon, Jacques D. Fleuriot:
  Higher Order Rippling in IsaPlanner. 83-98
  
• Ruben Gamboa, John R. Cowles:
  A Mechanical Proof of the Cook-Levin Theorem. 99-116
  
• Thomas C. Hales:
  Formalizing the Proof of the Kepler Conjecture. 117
  
• Nadeem Abdul Hamid, Zhong Shao:
  Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. 118-135
  
• Jason Hickey, Aleksey Nogin:
  Extensible Hierarchical Tactic Construction in a Logical Framework. 136-151
  
• Einar Broch Johnsen, Christoph Lüth:
  Theorem Reuse by Proof Term Transformation. 152-167
  
• Michael Jones, Aaron Benson, Dan Delorey:
  Proving Compatibility Using Refinement. 168-183
  
• Hanbing Liu, J. Strother Moore:
  Java Program Verification via a JVM Deep Embedding in ACL2. 184-200
  
• John Longley, Randy Pollack:
  Reasoning About CBV Functional Programs in Isabelle/HOL. 201-216
  
• Jean-François Monin:
  Proof Pearl: From Concrete to Functional Unparsing. 217-224
  
• Julien Narboux:
  A Decision Procedure for Geometry in Coq. 225-240
  
• Michael Norrish:
  Recursive Function Definition for Types with Binders. 241-256
  
• Lee Pike, Jeffrey Maddalon, Paul S. Miner, Alfons Geser:
  Abstractions for Fault-Tolerant Distributed System Verification. 257-270
  
• Stefan Richter:
  Formalizing Integration Theory with an Application to Probabilistic Algorithms. 271-286
  
• Tian-jun Zuo, Jun-gang Han, Ping Chen:
  Formalizing Java Dynamic Loading in HOL. 287-304
  
• Martin Wildmoser, Tobias Nipkow:
  Certifying Machine Code Safety: Shallow Versus Deep Embedding. 305-320
  
• Ting Zhang, Henny B. Sipma, Zohar Manna:
  Term Algebras with Length Function and Bounded Quantifier Alternation. 321-336