Conferences in DBLP

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

1. Jean-Raymond Abrial, Dominique Cansell
   Click'n Prove: Interactive Proofs within Set Theory. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:1-24 [Conf]
   
2. Anthony C. J. Fox
   Formal Specification and Verification of ARM6. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:25-40 [Conf]
   
3. Claire L. Quigley
   A Programming Logic for Java Bytecode Programs. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:41-54 [Conf]
   
4. Gerwin Klein, Martin Wildmoser
   Verified Bytecode Subroutines. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:55-70 [Conf]
   
5. Michael Norrish
   Complete Integer Decision Procedures as Derived Rules in HOL. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:71-86 [Conf]
   
6. Nicolas Magaud
   Changing Data Representation within the Coq System. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:87-102 [Conf]
   
7. Konrad Slind, Joe Hurd
   Applications of Polytypism in Theorem Proving. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:103-119 [Conf]
   
8. Carsten Schürmann, Frank Pfenning
   A Coverage Checking Algorithm for LF. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:120-135 [Conf]
   
9. Deepak Kapur, Nikita A. Sakhanenko
   Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2003, pp:136-154 [Conf]
   
10. David Cachera, David Pichardie
    Embedding of Systems of Affine Recurrence Equations in Coq. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:155-170 [Conf]
    
11. Hasan Amjad
    Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:171-187 [Conf]
    
12. Peter Dybjer, Qiao Haiyan, Makoto Takeyama
    Combining Testing and Proving in Dependent Type Theory. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:188-203 [Conf]
    
13. Dale Miller
    Reasoning about Proof Search Specifications: An Abstract. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:204- [Conf]
    
14. Luís Cruz-Filipe, Bas Spitters
    Program Extraction from Large Proof Developments. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:205-220 [Conf]
    
15. Freek Wiedijk, Jan Zwanenburg
    First Order Logic with Domain Conditions. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:221-237 [Conf]
    
16. Jason Reed
    Extending Higher-Order Unification to Support Proof Irrelevance. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:238-252 [Conf]
    
17. Sava Krstic, John Matthews
    Inductive Invariants for Nested Recursion. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:253-269 [Conf]
    
18. Jacek Chrzaszcz
    Implementing Modules in the Coq System. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:270-286 [Conf]
    
19. Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, Xin Yu
    MetaPRL - A Modular Logical Environment. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:287-303 [Conf]
    
20. Laurent Théry
    Proving Pearl: Knuth's Algorithm for Prime Numbers. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:304-318 [Conf]
    
21. Laura I. Meikle, Jacques D. Fleuriot
    Formalizing Hilbert's Grundlagen in Isabelle/Isar. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:319-334 [Conf]
    
22. June Andronick, Boutheina Chetali, Olivier Ly
    Using Coq to Verify Java Card Applet Isolation Properties. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:335-351 [Conf]
    
23. Giampaolo Bella, Cristiano Longo, Lawrence C. Paulson
    Verifying Second-Level Security Protocols. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2003, pp:352-366 [Conf]