TPHOLs 2004
Park City, Utah, USA
September 14-17, 2004
http://www.cs.utah.edu/tphols2004/
[
Home Page
]
[
Schedule
]
[
Hotel and Registration
]
[
Call for Papers
]
Accepted Papers
[
Travel to Park City
]
[
Conference History
]
[
Related Events
]
[
TPHOLs2005
]
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