| 2023 | ITP | POSIX Lexing with Bitcoded Derivatives. | Chengsong Tan, Christian Urban |
| 2017 | ECOOP | Modelling Homogeneous Generative Meta-Programming. | Martin Berger, Laurence Tratt, Christian Urban |
| 2016 | ITP | POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). | Fahad Ausaf, Roy Dyckhoff, Christian Urban |
| 2013 | CPP | A Formal Model and Correctness Proof for an Access Control Policy Framework. | Chunhan Wu, Xingyuan Zhang, Christian Urban |
| 2013 | ITP | Mechanising Turing Machines and Computability Theory in Isabelle/HOL. | Jian Xu, Xingyuan Zhang, Christian Urban |
| 2012 | ITP | Priority Inheritance Protocol Proved Correct. | Xingyuan Zhang, Christian Urban, Chunhan Wu |
| 2011 | CPP | Mechanizing the Metatheory of mini-XQuery. | James Cheney, Christian Urban |
| 2011 | ESOP | General Bindings and Alpha-Equivalence in Nominal Isabelle. | Christian Urban, Cezary Kaliszyk |
| 2011 | ITP | A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). | Chunhan Wu, Xingyuan Zhang, Christian Urban |
| 2011 | SAC | Quotients revisited for Isabelle/HOL. | Cezary Kaliszyk, Christian Urban |
| 2010 | ITP | A New Foundation for Nominal Isabelle. | Brian Huffman, Christian Urban |
| 2008 | AISC | Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. | Peter Chapman, James McKinna, Christian Urban |
| 2008 | LICS | Mechanizing the Metatheory of LF. | Christian Urban, James Cheney, Stefan Berghofer |
| 2007 | CADE | Barendregt's Variable Convention in Rule Inductions. | Christian Urban, Stefan Berghofer, Michael Norrish |
| 2006 | CADE | A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. | Christian Urban, Stefan Berghofer |
| 2005 | CADE | Nominal Techniques in Isabelle/HOL. | Christian Urban, Christine Tasson |
| 2005 | ICFP | A formal treatment of the barendregt variable convention in rule inductions. | Christian Urban, Michael Norrish |
| 2004 | ICLP | alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. | James Cheney, Christian Urban |
| 2003 | CSL | Nominal Unificaiton. | Christian Urban, Andrew M. Pitts, Murdoch Gabbay |
| 1998 | TABLEAUX | Implementation of Proof Search in the Imperative Programming Language Pizza. | Christian Urban |