Accepted Papers

• Behzad Akbarpour and Sofiene Tahar
  Error Analysis of Digital Filters using Theorem Proving

• Penny Anderson and Frank Pfenning
  Verifying Uniqueness in a Logical Framework

• David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, and Alberto Momigliano
  A Program Logic for Resource Verification

• Olivier Boite
  Proof Reuse with Extended Inductive Types

• Luis Cruz-Filipe and Freek Wiedijk
  Hierarchical Reflection

• Lucas Dixon and Jacques Fleuriot
  Higher Order Rippling in IsaPlanner

• Ruben Gamboa and John Cowles
  A Mechanical Proof of the Cook-Levin Theorem

• Nadeem Abdul Hamid and Zhong Shao
  Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code

• Jason Hickey and Aleksey Nogin
  Extensible Hierarchical Tactic Construction in a Logical Framework

• Einar Broch Johnsen and Christoph Lueth
  Theorem Reuse by Proof Term Transformation

• Michael Jones, Aaron Benson, and Dan Delorey
  Proving Compatibility using Refinement

• Hanbing Liu and J Moore
  Java Program Verification via a JVM Deep Embedding in ACL2

• John Longley and Randy Pollack
  Reasoning About CBV Functional Programs in Isabelle/HOL

• Jean-Francois Monin
  Proof Pearl: From concrete to functional unparsing

• Julien Narboux
  A Decision Procedure for Geometry in Coq

• Michael Norrish
  Recursive function definition for types with binders

• Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser
  Abstractions for Fault-Tolerant Distributed System Verification

• Stefan Richter
  Formalizing Integration Theory, with an Application to Probabilistic Algorithms

• Martin Wildmoser and Tobias Nipkow
  Certifying machine code safety: shallow versus deep embedding

• Ting Zhang, Henny B. Sipma, and Zohar Manna
  Term Algebras with Length Function and Bounded Quantifier Alternation

• Zuo Tian-Jun, Han Jun-Gang, and Chen Ping
  Formalizing Java Dynamic Loading in HOL

TPHOLs / tphols2004@cs.utah.edu