| 2009 |
|---|
| 25 | EE | Andreas Abel,
Christian Urban:
Preface.
Electr. Notes Theor. Comput. Sci. 228: 1 (2009) |
| 2008 |
|---|
| 24 | EE | Peter Chapman,
James McKinna,
Christian Urban:
Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle.
AISC/MKM/Calculemus 2008: 38-52 |
| 23 | EE | Christian Urban,
James Cheney,
Stefan Berghofer:
Mechanizing the Metatheory of LF.
LICS 2008: 45-56 |
| 22 | EE | Christian Urban,
Bozhi Zhu:
Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.
RTA 2008: 409-424 |
| 21 | EE | Stefan Berghofer,
Christian Urban:
Nominal Inversion Principles.
TPHOLs 2008: 71-85 |
| 20 | EE | James Cheney,
Christian Urban:
Nominal logic programming.
ACM Trans. Program. Lang. Syst. 30(5): (2008) |
| 19 | EE | Christian Urban,
James Cheney,
Stefan Berghofer:
Mechanizing the Metatheory of LF
CoRR abs/0804.1667: (2008) |
| 18 | EE | Julien Narboux,
Christian Urban:
Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking.
Electr. Notes Theor. Comput. Sci. 196: 3-18 (2008) |
| 17 | EE | Christian Urban:
Nominal Techniques in Isabelle/HOL.
J. Autom. Reasoning 40(4): 327-356 (2008) |
| 2007 |
|---|
| 16 | EE | Christian Urban,
Stefan Berghofer,
Michael Norrish:
Barendregt's Variable Convention in Rule Inductions.
CADE 2007: 35-50 |
| 15 | EE | Stefan Berghofer,
Christian Urban:
A Head-to-Head Comparison of de Bruijn Indices and Names.
Electr. Notes Theor. Comput. Sci. 174(5): 53-67 (2007) |
| 2006 |
|---|
| 14 | EE | Christian Urban,
Stefan Berghofer:
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL.
IJCAR 2006: 498-512 |
| 13 | EE | James Cheney,
Christian Urban:
Nominal Logic Programming
CoRR abs/cs/0609062: (2006) |
| 12 | EE | Gianluigi Bellin,
Martin Hyland,
Edmund Robinson,
Christian Urban:
Categorical proof theory of classical propositional calculus.
Theor. Comput. Sci. 364(2): 146-165 (2006) |
| 2005 |
|---|
| 11 | EE | Christian Urban,
Christine Tasson:
Nominal Techniques in Isabelle/HOL.
CADE 2005: 38-53 |
| 10 | EE | Christian Urban,
Michael Norrish:
A formal treatment of the barendregt variable convention in rule inductions.
MERLIN 2005: 25-32 |
| 9 | EE | Christian Urban,
James Cheney:
Avoiding Equivariance in Alpha-Prolog.
TLCA 2005: 401-416 |
| 2004 |
|---|
| 8 | EE | James Cheney,
Christian Urban:
alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence.
ICLP 2004: 269-283 |
| 7 | EE | Christian Urban,
Andrew M. Pitts,
Murdoch Gabbay:
Nominal unification.
Theor. Comput. Sci. 323(1-3): 473-497 (2004) |
| 2003 |
|---|
| 6 | EE | Christian Urban,
Andrew M. Pitts,
Murdoch Gabbay:
Nominal Unificaiton.
CSL 2003: 513-527 |
| 5 | EE | Roy Dyckhoff,
Christian Urban:
Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation.
J. Log. Comput. 13(5): 689-706 (2003) |
| 2001 |
|---|
| 4 | EE | Christian Urban:
Strong Normalisation for a Gentzen-like Cut-Elimination Procedure.
TLCA 2001: 415-430 |
| 3 | | Christian Urban,
Gavin M. Bierman:
Strong Normalisation of Cut-Elimination in Classical Logic.
Fundam. Inform. 45(1-2): 123-155 (2001) |
| 1999 |
|---|
| 2 | EE | Christian Urban,
Gavin M. Bierman:
Strong Normalisation of Cut-Elimination in Classical Logic.
TLCA 1999: 365-380 |
| 1998 |
|---|
| 1 | EE | Christian Urban:
Implementation of Proof Search in the Imperative Programming Language Pizza.
TABLEAUX 1998: 313-319 |
