Search the dblp DataBase

Publications of Author

1. Christian Urban, Stefan Berghofer
   A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
   IJCAR, 2006, pp:498-512 [Conf]
   
2. Christian Urban, Christine Tasson
   Nominal Techniques in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
   CADE, 2005, pp:38-53 [Conf]
   
3. Christian Urban, Andrew M. Pitts, Murdoch Gabbay
   Nominal Unificaiton. [Citation Graph (0, 0)][DBLP]
   CSL, 2003, pp:513-527 [Conf]
   
4. James Cheney, Christian Urban
   alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. [Citation Graph (0, 0)][DBLP]
   ICLP, 2004, pp:269-283 [Conf]
   
5. Christian Urban
   Implementation of Proof Search in the Imperative Programming Language Pizza. [Citation Graph (0, 0)][DBLP]
   TABLEAUX, 1998, pp:313-319 [Conf]
   
6. Christian Urban
   Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. [Citation Graph (0, 0)][DBLP]
   TLCA, 2001, pp:415-430 [Conf]
   
7. Christian Urban, Gavin M. Bierman
   Strong Normalisation of Cut-Elimination in Classical Logic. [Citation Graph (0, 0)][DBLP]
   TLCA, 1999, pp:365-380 [Conf]
   
8. Christian Urban, James Cheney
   Avoiding Equivariance in Alpha-Prolog. [Citation Graph (0, 0)][DBLP]
   TLCA, 2005, pp:401-416 [Conf]
   
9. Stefan Berghofer, Christian Urban
   A Head-to-Head Comparison of de Bruijn Indices and Names. [Citation Graph (0, 0)][DBLP]
   Electr. Notes Theor. Comput. Sci., 2007, v:174, n:5, pp:53-67 [Journal]
   
10. Christian Urban, Gavin M. Bierman
    Strong Normalisation of Cut-Elimination in Classical Logic. [Citation Graph (0, 0)][DBLP]
    Fundam. Inform., 2001, v:45, n:1-2, pp:123-155 [Journal]
    
11. Roy Dyckhoff, Christian Urban
    Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation. [Citation Graph (0, 0)][DBLP]
    J. Log. Comput., 2003, v:13, n:5, pp:689-706 [Journal]
    
12. Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban
    Categorical proof theory of classical propositional calculus. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 2006, v:364, n:2, pp:146-165 [Journal]
    
13. Christian Urban, Andrew M. Pitts, Murdoch Gabbay
    Nominal unification. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 2004, v:323, n:1-3, pp:473-497 [Journal]
    
14. Christian Urban, Stefan Berghofer, Michael Norrish
    Barendregt's Variable Convention in Rule Inductions. [Citation Graph (0, 0)][DBLP]
    CADE, 2007, pp:35-50 [Conf]
    
15. James Cheney, Christian Urban
    Nominal Logic Programming [Citation Graph (0, 0)][DBLP]
    CoRR, 2006, v:0, n:, pp:- [Journal]
    
16. 
    Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. [Citation Graph (, )][DBLP]
    
    
17. 
    A formal treatment of the barendregt variable convention in rule inductions. [Citation Graph (, )][DBLP]
    
    
18. 
    Mechanizing the Metatheory of LF. [Citation Graph (, )][DBLP]
    
    
19. 
    Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. [Citation Graph (, )][DBLP]
    
    
20. 
    Nominal Inversion Principles. [Citation Graph (, )][DBLP]
    
    
21. 
    A New Foundation for Nominal Isabelle. [Citation Graph (, )][DBLP]
    
    
22. 
    Mechanizing the Metatheory of LF [Citation Graph (, )][DBLP]
    
    
23. 
    Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. [Citation Graph (, )][DBLP]
    
    
24. 
    Preface. [Citation Graph (, )][DBLP]
    
    
25. 
    Formal SOS-Proofs for the Lambda-Calculus. [Citation Graph (, )][DBLP]