Conferences in DBLP

International Conference on Theorem Proving in Higher Order Logics (tphol)
2004 (conf/tphol/2004)

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