17. TPHOLs 2004:
Park City, Utah, USA
Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (Eds.):
Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings.
Lecture Notes in Computer Science 3223 Springer 2004, ISBN 3-540-23017-3 
- 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
Last update Fri May 17 16:21:41 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
