17. TPHOLs 2004: Park City, Utah, USA

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