Christian Urban

Christian Urban, Cezary Kaliszyk: General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science 8(2) (2012)

Maribel Fernández, Christian Urban: Preface: Theory and Applications of Abstraction, Substitution and Naming. J. Autom. Reasoning 49(2): 111-114 (2012)

Xingyuan Zhang, Christian Urban, Chunhan Wu: Priority Inheritance Protocol Proved Correct. ITP 2012: 217-232

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

Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the metatheory of LF. ACM Trans. Comput. Log. 12(2): 15 (2011)

James Cheney, Christian Urban: Mechanizing the Metatheory of mini-XQuery. CPP 2011: 280-295

Christian Urban, Cezary Kaliszyk: General Bindings and Alpha-Equivalence in Nominal Isabelle. ESOP 2011: 480-500

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

Cezary Kaliszyk, Christian Urban: Quotients revisited for Isabelle/HOL. SAC 2011: 1639-1644

Brian Huffman, Christian Urban: A New Foundation for Nominal Isabelle. ITP 2010: 35-50

Christian Urban: Nominal Unification Revisited. UNIF 2010: 1-11

Andreas Abel, Christian Urban: Preface. Electr. Notes Theor. Comput. Sci. 228: 1 (2009)

Christian Urban, Julien Narboux: Formal SOS-Proofs for the Lambda-Calculus. Electr. Notes Theor. Comput. Sci. 247: 139-155 (2009)

Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (Eds.): Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science 5674, Springer 2009, isbn 978-3-642-03358-2

Julien Narboux, Christian Urban: Formalising in Nominal Isabelle Crary's Completeness Proof for Equivalence Checking. Electr. Notes Theor. Comput. Sci. 196: 3-18 (2008)

Christian Urban: Nominal Techniques in Isabelle/HOL. J. Autom. Reasoning 40(4): 327-356 (2008)

James Cheney, Christian Urban: Nominal logic programming. ACM Trans. Program. Lang. Syst. 30(5) (2008)

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

Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the Metatheory of LF. LICS 2008: 45-56

Christian Urban, Bozhi Zhu: Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof. RTA 2008: 409-424

Stefan Berghofer, Christian Urban: Nominal Inversion Principles. TPHOLs 2008: 71-85

Christian Urban, James Cheney, Stefan Berghofer: Mechanizing the Metatheory of LF. CoRR abs/0804.1667 (2008)

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)

Christian Urban, Stefan Berghofer, Michael Norrish: Barendregt's Variable Convention in Rule Inductions. CADE 2007: 35-50

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

Christian Urban, Stefan Berghofer: A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. IJCAR 2006: 498-512

James Cheney, Christian Urban: Nominal Logic Programming. CoRR abs/cs/0609062 (2006)

Christian Urban, Christine Tasson: Nominal Techniques in Isabelle/HOL. CADE 2005: 38-53

Christian Urban, Michael Norrish: A formal treatment of the barendregt variable convention in rule inductions. MERLIN 2005: 25-32

Christian Urban, James Cheney: Avoiding Equivariance in Alpha-Prolog. TLCA 2005: 401-416

Christian Urban, Andrew M. Pitts, Murdoch Gabbay: Nominal unification. Theor. Comput. Sci. 323(1-3): 473-497 (2004)

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

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

Christian Urban, Andrew M. Pitts, Murdoch Gabbay: Nominal Unificaiton. CSL 2003: 513-527

Christian Urban, Gavin M. Bierman: Strong Normalisation of Cut-Elimination in Classical Logic. Fundam. Inform. 45(1-2): 123-155 (2001)

Christian Urban: Strong Normalisation for a Gentzen-like Cut-Elimination Procedure. TLCA 2001: 415-430

Christian Urban, Gavin M. Bierman: Strong Normalisation of Cut-Elimination in Classical Logic. TLCA 1999: 365-380

Christian Urban: Implementation of Proof Search in the Imperative Programming Language Pizza. TABLEAUX 1998: 313-319