Implementation of Proof Search in the Imperative Programming Language Pizza. - Christian Urban (TABLEAUX, 1998)

Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. - Christian Urban (TLCA, 2001)

Strong Normalisation of Cut-Elimination in Classical Logic. - Christian Urban; Gavin M. Bierman (Fundam. Informaticae, 2001)

Nominal Unificaiton. - Christian Urban; Andrew M. Pitts; Murdoch Gabbay (CSL, 2003)

Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation. - Roy Dyckhoff; Christian Urban (J. Log. Comput., 2003)

alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence. - James Cheney; Christian Urban (ICLP, 2004)

Nominal unification. - Christian Urban; Andrew M. Pitts; Murdoch Gabbay (Theor. Comput. Sci., 2004)

Nominal Techniques in Isabelle/HOL. - Christian Urban; Christine Tasson (CADE, 2005)

A formal treatment of the barendregt variable convention in rule inductions. - Christian Urban; Michael Norrish (MERLIN, 2005)

Avoiding Equivariance in Alpha-Prolog. - Christian Urban; James Cheney (TLCA, 2005)

A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. - Christian Urban; Stefan Berghofer (IJCAR, 2006)

A Head-to-Head Comparison of de Bruijn Indices and Names. - Stefan Berghofer; Christian Urban (LFMTP@FLoC, 2006)

Categorical proof theory of classical propositional calculus. - Gianluigi Bellin; Martin Hyland; Edmund Robinson; Christian Urban (Theor. Comput. Sci., 2006)

Barendregt's Variable Convention in Rule Inductions. - Christian Urban; Stefan Berghofer; Michael Norrish (CADE, 2007)

Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. - Julien Narboux; Christian Urban (LFMTP@CADE, 2007)

Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle. - Peter Chapman; James McKinna; Christian Urban (AISC/MKM/Calculemus, 2008)

Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. - Christian Urban; Bozhi Zhu (RTA, 2008)

Nominal Inversion Principles. - Stefan Berghofer; Christian Urban (TPHOLs, 2008)

Preface. - Andreas Abel 001; Christian Urban (LFMTP@LICS, 2008)

Formal SOS-Proofs for the Lambda-Calculus. - Christian Urban; Julien Narboux (LSFA, 2008)

Nominal Techniques in Isabelle/HOL. - Christian Urban (J. Autom. Reason., 2008)

Nominal logic programming. - James Cheney; Christian Urban (ACM Trans. Program. Lang. Syst., 2008)

A New Foundation for Nominal Isabelle. - Brian Huffman; Christian Urban (ITP, 2010)

Nominal Unification Revisited - Christian Urban (UNIF, 2010)

Mechanizing the Metatheory of mini-XQuery. - James Cheney; Christian Urban (CPP, 2011)

A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). - Chunhan Wu; Xingyuan Zhang; Christian Urban (ITP, 2011)

Quotients revisited for Isabelle/HOL. - Cezary Kaliszyk; Christian Urban (SAC, 2011)

The Myhill-Nerode Theorem Based on Regular Expressions. - Chunhan Wu; Xingyuan Zhang; Christian Urban (Arch. Formal Proofs, 2011)

Mechanizing the metatheory of LF. - Christian Urban; James Cheney; Stefan Berghofer (ACM Trans. Comput. Log., 2011)

General Bindings and Alpha-Equivalence in Nominal Isabelle - Christian Urban; Cezary Kaliszyk (Log. Methods Comput. Sci., 2012)

Preface: Theory and Applications of Abstraction, Substitution and Naming. - Maribel Fernández; Christian Urban (J. Autom. Reason., 2012)

A Formal Model and Correctness Proof for an Access Control Policy Framework. - Chunhan Wu; Xingyuan Zhang; Christian Urban (CPP, 2013)

Mechanising Turing Machines and Computability Theory in Isabelle/HOL. - Jian Xu; Xingyuan Zhang; Christian Urban (ITP, 2013)

A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions. - Chunhan Wu; Xingyuan Zhang; Christian Urban (J. Autom. Reason., 2014)

POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl). - Fahad Ausaf; Roy Dyckhoff; Christian Urban (ITP, 2016)

POSIX Lexing with Derivatives of Regular Expressions. - Fahad Ausaf; Roy Dyckhoff; Christian Urban (Arch. Formal Proofs, 2016)

Modelling Homogeneous Generative Meta-Programming. - Martin Berger 001; Laurence Tratt; Christian Urban (ECOOP, 2017)

Universal Turing Machine. - Jian Xu; Xingyuan Zhang; Christian Urban; Sebastiaan J. C. Joosten (Arch. Formal Proofs, 2019)

Selected Extended Papers of ITP 2015: Preface. - Xingyuan Zhang; Christian Urban (J. Autom. Reason., 2019)

Priority Inheritance Protocol Proved Correct. - Xingyuan Zhang; Christian Urban; Chunhan Wu (J. Autom. Reason., 2020)

POSIX Lexing with Bitcoded Derivatives. - Chengsong Tan; Christian Urban (ITP, 2023)

POSIX Lexing with Derivatives of Regular Expressions. - Christian Urban (J. Autom. Reason., 2023)